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 = ()

18


19

(* Format.eprintf "%a" *)

20

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

21

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

22

redefinition allowed. *)

23


24

open Utils

25


26

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

27

yet this makes notations far lighter.*)

28

open Lustre_types

29

open Corelang

30


31

(* TODO general remark: except in the add_vdecl, it seems to me that all the

32

pairs (env, vd_env) should be replace with just env, since vd_env is never

33

used and the env element is always extract with a fst *)

34


35

module type EXPR_TYPE_HUB = sig

36

type type_expr

37


38

val import : Types.Main.type_expr > type_expr

39


40

val export : type_expr > Types.Main.type_expr

41

end

42


43

module Make

44

(T : Types.S)

45

(Expr_type_hub : EXPR_TYPE_HUB with type type_expr = T.type_expr) =

46

struct

47

module TP = Type_predef.Make (T)

48

include TP

49


50

let pp_typing_env fmt env = Env.pp_env print_ty fmt env

51


52

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

53

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

54

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

55


56

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

57

[ty]. False otherwise. *)

58

let rec occurs tvar ty =

59

let ty = repr ty in

60

match type_desc ty with

61

 Tvar >

62

ty = tvar

63

 Tarrow (t1, t2) >

64

occurs tvar t1  occurs tvar t2

65

 Ttuple tl >

66

List.exists (occurs tvar) tl

67

 Tstruct fl >

68

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

69

 Tarray (_, t)  Tstatic (_, t)  Tclock t  Tlink t >

70

occurs tvar t

71

 Tenum _  Tconst _  Tunivar  Tbasic _ >

72

false

73


74

(* Generalize by sideeffects *)

75


76

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

77

let rec generalize ty =

78

match type_desc ty with

79

 Tvar >

80

(* No scopes, always generalize *)

81

ty.tdesc < Tunivar

82

 Tarrow (t1, t2) >

83

generalize t1;

84

generalize t2

85

 Ttuple tl >

86

List.iter generalize tl

87

 Tstruct fl >

88

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

89

 Tstatic (d, t)  Tarray (d, t) >

90

Dimension.generalize d;

91

generalize t

92

 Tclock t  Tlink t >

93

generalize t

94

 Tenum _  Tconst _  Tunivar  Tbasic _ >

95

()

96


97

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

98

let rec instantiate inst_vars inst_dim_vars ty =

99

let ty = repr ty in

100

match ty.tdesc with

101

 Tenum _  Tconst _  Tvar  Tbasic _ >

102

ty

103

 Tarrow (t1, t2) >

104

{

105

ty with

106

tdesc =

107

Tarrow

108

( instantiate inst_vars inst_dim_vars t1,

109

instantiate inst_vars inst_dim_vars t2 );

110

}

111

 Ttuple tlist >

112

{

113

ty with

114

tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist);

115

}

116

 Tstruct flist >

117

{

118

ty with

119

tdesc =

120

Tstruct

121

(List.map

122

(fun (f, t) > f, instantiate inst_vars inst_dim_vars t)

123

flist);

124

}

125

 Tclock t >

126

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

127

 Tstatic (d, t) >

128

{

129

ty with

130

tdesc =

131

Tstatic

132

( Dimension.instantiate inst_dim_vars d,

133

instantiate inst_vars inst_dim_vars t );

134

}

135

 Tarray (d, t) >

136

{

137

ty with

138

tdesc =

139

Tarray

140

( Dimension.instantiate inst_dim_vars d,

141

instantiate inst_vars inst_dim_vars t );

142

}

143

 Tlink t >

144

(* should not happen *)

145

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

146

 Tunivar > (

147

try List.assoc ty.tid !inst_vars

148

with Not_found >

149

let var = new_var () in

150

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

151

var)

152


153

let basic_coretype_type t =

154

if is_real_type t then Tydec_real

155

else if is_int_type t then Tydec_int

156

else if is_bool_type t then Tydec_bool

157

else assert false

158


159

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

160

let rec type_coretype type_dim cty =

161

match (*get_repr_type*)

162

cty with

163

 Tydec_any >

164

new_var ()

165

 Tydec_int >

166

type_int

167

 Tydec_real >

168

(* Type_predef. *)

169

type_real

170

(*  Tydec_float > Type_predef.type_real *)

171

 Tydec_bool >

172

(* Type_predef. *)

173

type_bool

174

 Tydec_clock ty >

175

(* Type_predef. *)

176

type_clock (type_coretype type_dim ty)

177

 Tydec_const c >

178

(* Type_predef. *)

179

type_const c

180

 Tydec_enum tl >

181

(* Type_predef. *)

182

type_enum tl

183

 Tydec_struct fl >

184

(* Type_predef. *)

185

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

186

 Tydec_array (d, ty) >

187

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

188

type_dim d;

189

(* Type_predef. *)

190

type_array d (type_coretype type_dim ty)

191


192

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

193

let rec coretype_type ty =

194

match (repr ty).tdesc with

195

 Tvar >

196

Tydec_any

197

 Tbasic _ >

198

basic_coretype_type ty

199

 Tconst c >

200

Tydec_const c

201

 Tclock t >

202

Tydec_clock (coretype_type t)

203

 Tenum tl >

204

Tydec_enum tl

205

 Tstruct fl >

206

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

207

 Tarray (d, t) >

208

Tydec_array (d, coretype_type t)

209

 Tstatic (_, t) >

210

coretype_type t

211

 _ >

212

assert false

213


214

let get_coretype_definition tname =

215

try

216

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

217

match top.top_decl_desc with

218

 TypeDef tdef >

219

tdef.tydef_desc

220

 _ >

221

assert false

222

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

223


224

let get_type_definition tname =

225

type_coretype (fun _ > ()) (get_coretype_definition tname)

226


227

(* Equality on ground types only *)

228

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

229

let rec eq_ground t1 t2 =

230

let t1 = repr t1 in

231

let t2 = repr t2 in

232

t1 == t2

233



234

match t1.tdesc, t2.tdesc with

235

 Tbasic t1, Tbasic t2 when t1 == t2 >

236

true

237

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

238

true

239

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

240

List.for_all2 eq_ground tl tl'

241

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

242

List.for_all2 (fun (_, t) (_, t') > eq_ground t t') fl fl'

243

 Tconst t, _ >

244

let def_t = get_type_definition t in

245

eq_ground def_t t2

246

 _, Tconst t >

247

let def_t = get_type_definition t in

248

eq_ground t1 def_t

249

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

250

eq_ground t1 t1' && eq_ground t2 t2'

251

 Tclock t1', Tclock t2' >

252

eq_ground t1' t2'

253

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

254

>

255

Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'

256

 _ >

257

false

258


259

(** [unify t1 t2] unifies types [t1] and [t2] using standard destructive

260

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

261

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

262

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

263

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

264

unification is required, [t1] should furthermore be an instance of [t2]

265

and constants are handled differently.*)

266

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

267

let rec unif t1 t2 =

268

let t1 = repr t1 in

269

let t2 = repr t2 in

270

if t1 == t2 then ()

271

else

272

match t1.tdesc, t2.tdesc with

273

(* strictly subtyping cases first *)

274

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

275

unif t1 t2

276

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

277

unif t1 t2

278

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

279

 Tvar, Tvar >

280

if t1.tid < t2.tid then t2.tdesc < Tlink t1 else t1.tdesc < Tlink t2

281

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

282

t1.tdesc < Tlink t2

283

 _, Tvar when not (occurs t2 t1) >

284

t2.tdesc < Tlink t1

285

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

286

unif t2 t2';

287

unif t1' t1

288

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

289

List.iter2 unif tl tl'

290

 Ttuple [ t1 ], _ >

291

unif t1 t2

292

 _, Ttuple [ t2 ] >

293

unif t1 t2

294

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

295

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

296

 Tclock _, Tstatic _  Tstatic _, Tclock _ >

297

raise (Unify (t1, t2))

298

 Tclock t1', Tclock t2' >

299

unif t1' t2'

300

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

301

 Tunivar, _  _, Tunivar >

302

()

303

 Tconst t, _ >

304

let def_t = get_type_definition t in

305

unif def_t t2

306

 _, Tconst t >

307

let def_t = get_type_definition t in

308

unif t1 def_t

309

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

310

()

311

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

312

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

313

let eval_const =

314

if semi then fun c >

315

Some (Dimension.mkdim_ident Location.dummy_loc c)

316

else fun _ > None

317

in

318

unif t1' t2';

319

Dimension.eval Basic_library.eval_dim_env eval_const e1;

320

Dimension.eval Basic_library.eval_dim_env eval_const e2;

321

Dimension.unify ~semi e1 e2

322

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

323

for numerical constants with non static ones for variables with

324

possible machine types *)

325

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

326

BasicT.unify bt1 bt2

327

 _, _ >

328

raise (Unify (t1, t2))

329

in

330

unif t1 t2

331


332

(* Expected type ty1, got type ty2 *)

333

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

334

try unify ~sub ~semi ty1 ty2 with

335

 Unify _ >

336

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

337

 Dimension.Unify _ >

338

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

339


340

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

341

(* Typing function for each basic AST construct *)

342

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

343


344

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

345

if Hashtbl.mem field_table label then (

346

let tydef = Hashtbl.find field_table label in

347

let tydec = (typedef_of_top tydef).tydef_desc in

348

let tydec_struct = get_struct_type_fields tydec in

349

let ty_label =

350

type_coretype (fun _ > ()) (List.assoc label tydec_struct)

351

in

352

try_unify ty_label (type_const ~is_annot loc c) loc;

353

type_coretype (fun _ > ()) tydec)

354

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

355


356

and type_const ?(is_annot = false) loc c =

357

match c with

358

 Const_int _ >

359

(* Type_predef. *)

360

type_int

361

 Const_real _ >

362

(* Type_predef. *)

363

type_real

364

 Const_array ca >

365

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

366

let ty = new_var () in

367

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

368

(* Type_predef. *)

369

type_array d ty

370

 Const_tag t >

371

if Hashtbl.mem tag_table t then

372

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

373

let tydec =

374

if is_user_type tydef.tydef_desc then Tydec_const tydef.tydef_id

375

else tydef.tydef_desc

376

in

377

type_coretype (fun _ > ()) tydec

378

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

379

 Const_struct fl > (

380

let ty_struct = new_var () in

381

let used =

382

List.fold_left

383

(fun acc (l, c) >

384

if List.mem l acc then

385

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

386

else

387

try_unify ty_struct

388

(type_struct_const_field ~is_annot loc (l, c))

389

loc;

390

l :: acc)

391

[] fl

392

in

393

try

394

let total =

395

List.map fst (get_struct_type_fields (coretype_type ty_struct))

396

in

397

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

398

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

399

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

400

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

401

with Not_found > ty_struct)

402

 Const_string s  Const_modeid s >

403

if is_annot then (* Type_predef. *)

404

type_string

405

else (

406

Format.eprintf "Typing string %s outisde of annot scope@.@?" s;

407

assert false (* string datatype should only appear in annotations *))

408


409

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

410

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

411

is a pair composed of:  a map from ident to type, associating to each

412

ident, i.e. variables, constants and (imported) nodes, its type including

413

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

414

constant propagation policy in Lustre.  a vdecl list, in order to modify

415

types of declared variables that are later discovered to be clocks during

416

the typing process. *)

417

let check_constant loc const_expected const_real =

418

if const_expected && not const_real then raise (Error (loc, Not_a_constant))

419


420

let rec type_add_const env const arg targ =

421

(*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg

422

Types.print_ty targ;*)

423

if const then (

424

let d =

425

if is_dimension_type targ then dimension_of_expr arg

426

else Dimension.mkdim_var ()

427

in

428

let eval_const id =

429

(* Types. *)

430

get_static_value (Env.lookup_value (fst env) id)

431

in

432

Dimension.eval Basic_library.eval_dim_env eval_const d;

433

let real_static_type =

434

(* Type_predef. *)

435

type_static d ((* Types. *)

436

dynamic_type targ)

437

in

438

(match (* Types. *)

439

get_static_value targ with

440

 None >

441

()

442

 Some _ >

443

try_unify targ real_static_type arg.expr_loc);

444

real_static_type)

445

else targ

446


447

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

448

applications and assignments *)

449

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

450

let loc = real_arg.expr_loc in

451

let const =

452

const

453

 (* Types. *)

454

get_static_value formal_type <> None

455

in

456

let real_type =

457

type_add_const env const real_arg (type_expr env in_main const real_arg)

458

in

459

(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const

460

Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty

461

formal_type;*)

462

try_unify ~sub formal_type real_type loc

463


464

(* typing an application implies:  checking that const formal parameters

465

match real const (maybe symbolic) arguments  checking type adequation

466

between formal and real arguments An application may embed an

467

homomorphic/internal function, in which case we need to split it in many

468

calls *)

469

and type_appl env in_main loc const f args =

470

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

471

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

472

then

473

try

474

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

475

(* Types. *)

476

type_of_type_list

477

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

478

with Utils.TransposeError (l, l') >

479

raise (Error (loc, WrongMorphism (l, l')))

480

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

481


482

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

483

(argument, type) pairs. *)

484

and type_dependent_call env in_main loc const f targs =

485

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

486

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

487

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

488

let tfun =

489

(* Type_predef. *)

490

type_arrow tins touts

491

in

492

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

493

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

494

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

495

let tins = type_list_of_type tins in

496

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

497

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

498

else (

499

List.iter2

500

(fun (a, t) ti >

501

let t' =

502

type_add_const env

503

(const

504

 (* Types. *)

505

get_static_value ti <> None)

506

a t

507

in

508

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

509

print_ty t' print_ty touts; *)

510

try_unify ~sub:true ti t' a.expr_loc

511

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

512

print_ty t' print_ty touts; *))

513

targs tins;

514

touts)

515


516

(* type a simple call without dependent types but possible homomorphic

517

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

518

and type_simple_call env in_main loc const f targs =

519

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

520

let tfun =

521

(* Type_predef. *)

522

type_arrow tins touts

523

in

524

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

525

(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty

526

(type_of_type_list targs);*)

527

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

528

touts

529


530

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

531

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

532

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

533

let resulting_ty =

534

match expr.expr_desc with

535

 Expr_const c >

536

let ty = type_const ~is_annot expr.expr_loc c in

537

let ty =

538

(* Type_predef. *)

539

type_static (Dimension.mkdim_var ()) ty

540

in

541

expr.expr_type < Expr_type_hub.export ty;

542

ty

543

 Expr_ident v >

544

let tyv =

545

try Env.lookup_value (fst env) v

546

with Not_found >

547

Format.eprintf

548

"Failure in typing expr %a. Not in typing environement@."

549

Printers.pp_expr expr;

550

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

551

in

552

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

553

let ty' =

554

if const then

555

(* Type_predef. *)

556

type_static (Dimension.mkdim_var ()) (new_var ())

557

else new_var ()

558

in

559

try_unify ty ty' expr.expr_loc;

560

expr.expr_type < Expr_type_hub.export ty;

561

ty

562

 Expr_array elist >

563

let ty_elt = new_var () in

564

List.iter

565

(fun e >

566

try_unify ty_elt

567

(type_appl env in_main expr.expr_loc const "uminus" [ e ])

568

e.expr_loc)

569

elist;

570

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

571

let ty =

572

(* Type_predef. *)

573

type_array d ty_elt

574

in

575

expr.expr_type < Expr_type_hub.export ty;

576

ty

577

 Expr_access (e1, d) >

578

type_subtyping_arg env in_main false

579

(* not necessary a constant *)

580

(expr_of_dimension d)

581

(* Type_predef. *)

582

type_int;

583

let ty_elt = new_var () in

584

let d = Dimension.mkdim_var () in

585

type_subtyping_arg env in_main const e1

586

((* Type_predef. *)

587

type_array d ty_elt);

588

expr.expr_type < Expr_type_hub.export ty_elt;

589

ty_elt

590

 Expr_power (e1, d) >

591

let eval_const id =

592

(* Types. *)

593

get_static_value (Env.lookup_value (fst env) id)

594

in

595

type_subtyping_arg env in_main true (expr_of_dimension d)

596

(* Type_predef. *)

597

type_int;

598

Dimension.eval Basic_library.eval_dim_env eval_const d;

599

let ty_elt =

600

type_appl env in_main expr.expr_loc const "uminus" [ e1 ]

601

in

602

let ty =

603

(* Type_predef. *)

604

type_array d ty_elt

605

in

606

expr.expr_type < Expr_type_hub.export ty;

607

ty

608

 Expr_tuple elist >

609

let ty =

610

new_ty

611

(Ttuple (List.map (type_expr ~is_annot env in_main const) elist))

612

in

613

expr.expr_type < Expr_type_hub.export ty;

614

ty

615

 Expr_ite (c, t, e) >

616

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

617

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

618

expr.expr_type < Expr_type_hub.export ty;

619

ty

620

 Expr_appl (id, args, r) >

621

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

622

expression *)

623

(match r with

624

 None >

625

()

626

 Some c >

627

check_constant expr.expr_loc const false;

628

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

629

let args_list = expr_list_of_expr args in

630

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

631

let targs =

632

new_ty

633

(Ttuple

634

(List.map (fun a > Expr_type_hub.import a.expr_type) args_list))

635

in

636

args.expr_type < Expr_type_hub.export targs;

637

expr.expr_type < Expr_type_hub.export touts;

638

touts

639

 Expr_fby (e1, e2)  Expr_arrow (e1, e2) >

640

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

641

check_constant expr.expr_loc const false;

642

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

643

expr.expr_type < Expr_type_hub.export ty;

644

ty

645

 Expr_pre e >

646

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

647

check_constant expr.expr_loc const false;

648

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

649

expr.expr_type < Expr_type_hub.export ty;

650

ty

651

 Expr_when (e1, c, l) >

652

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

653

check_constant expr.expr_loc const false;

654

let typ_l =

655

(* Type_predef. *)

656

type_clock (type_const ~is_annot expr.expr_loc (Const_tag l))

657

in

658

let expr_c = expr_of_ident c expr.expr_loc in

659

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

660

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

661

expr.expr_type < Expr_type_hub.export ty;

662

ty

663

 Expr_merge (c, hl) >

664

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

665

check_constant expr.expr_loc const false;

666

let typ_in, typ_out =

667

type_branches env in_main expr.expr_loc const hl

668

in

669

let expr_c = expr_of_ident c expr.expr_loc in

670

let typ_l =

671

(* Type_predef. *)

672

type_clock typ_in

673

in

674

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

675

expr.expr_type < Expr_type_hub.export typ_out;

676

typ_out

677

in

678

Log.report ~level:3 (fun fmt >

679

Format.fprintf fmt "Type of expr %a: %a@ " Printers.pp_expr expr

680

(* Types. *)

681

print_ty resulting_ty);

682

resulting_ty

683


684

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

685

let typ_in = new_var () in

686

let typ_out = new_var () in

687

try

688

let used_labels =

689

List.fold_left

690

(fun accu (t, h) >

691

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

692

type_subtyping_arg env in_main const h typ_out;

693

if List.mem t accu then raise (Error (loc, Already_bound t))

694

else t :: accu)

695

[] hl

696

in

697

let type_labels = get_enum_type_tags (coretype_type typ_in) in

698

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

699

let unbound_tag =

700

List.find (fun t > not (List.mem t used_labels)) type_labels

701

in

702

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

703

else typ_in, typ_out

704

with Unify (t1, t2) > raise (Error (loc, Type_clash (t1, t2)))

705


706

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

707

env *)

708

let type_eexpr env eexpr =

709

type_expr ~is_annot:true env false (* not in main *) false (* not a const *)

710

eexpr.eexpr_qfexpr

711


712

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

713

let type_eq env in_main undefined_vars eq =

714

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

715

(* Check undefined variables, type lhs *)

716

let expr_lhs =

717

expr_of_expr_list eq.eq_loc

718

(List.map (fun v > expr_of_ident v eq.eq_loc) eq.eq_lhs)

719

in

720

let ty_lhs = type_expr env in_main false expr_lhs in

721

(* Check multiple variable definitions *)

722

let define_var id uvars =

723

if ISet.mem id uvars then ISet.remove id uvars

724

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

725

in

726

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

727

let ty_lhs =

728

type_of_type_list

729

(List.map2

730

(fun ty id >

731

if get_static_value ty <> None then

732

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

733

else match get_clock_base_type ty with None > ty  Some ty > ty)

734

(type_list_of_type ty_lhs) eq.eq_lhs)

735

in

736

let undefined_vars =

737

List.fold_left

738

(fun uvars v > define_var v uvars)

739

undefined_vars eq.eq_lhs

740

in

741

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

742

assigned to a (always nonconstant) lhs variable *)

743

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

744

undefined_vars

745


746

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

747

environment [env] *)

748

let type_coreclock env ck id loc =

749

match ck.ck_dec_desc with

750

 Ckdec_any >

751

()

752

 Ckdec_bool cl >

753

let dummy_id_expr = expr_of_ident id loc in

754

let when_expr =

755

List.fold_left

756

(fun expr (x, l) >

757

{

758

expr_tag = new_tag ();

759

expr_desc = Expr_when (expr, x, l);

760

expr_type = Types.Main.new_var ();

761

expr_clock = Clocks.new_var true;

762

expr_delay = Delay.new_var ();

763

expr_loc = loc;

764

expr_annot = None;

765

})

766

dummy_id_expr cl

767

in

768

ignore (type_expr env false false when_expr)

769


770

let rec check_type_declaration loc cty =

771

match cty with

772

 Tydec_clock ty  Tydec_array (_, ty) >

773

check_type_declaration loc ty

774

 Tydec_const tname >

775

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

776

if not (Hashtbl.mem type_table cty) then

777

raise (Error (loc, Unbound_type tname))

778

 _ >

779

()

780


781

let type_var_decl vd_env env vdecl =

782

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

783

Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)

784

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

785

let eval_const id =

786

(* Types. *)

787

get_static_value (Env.lookup_value env id)

788

in

789

let type_dim d =

790

type_subtyping_arg (env, vd_env) false true (expr_of_dimension d)

791

(* Type_predef. *)

792

type_int;

793

Dimension.eval Basic_library.eval_dim_env eval_const d

794

in

795

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

796


797

let ty_static =

798

if vdecl.var_dec_const then

799

(* Type_predef. *)

800

type_static (Dimension.mkdim_var ()) ty

801

else ty

802

in

803

(match vdecl.var_dec_value with

804

 None >

805

()

806

 Some v >

807

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

808

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

809

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

810

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

811

vdecl.var_loc;

812

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

813

new_env

814


815

let type_var_decl_list vd_env env l =

816

List.fold_left (type_var_decl vd_env) env l

817


818

let type_of_vlist vars =

819

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

820

type_of_type_list tyl

821


822

let add_vdecl vd_env vdecl =

823

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

824

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

825

else vdecl :: vd_env

826


827

let check_vd_env vd_env = ignore (List.fold_left add_vdecl [] vd_env)

828


829

let type_contract env c =

830

let vd_env = c.consts @ c.locals in

831

check_vd_env vd_env;

832

let env =

833

type_var_decl_list

834

(* this argument seems useless to me, cf TODO at top of the file*)

835

vd_env env vd_env

836

in

837

(* typing stmts *)

838

let eqs =

839

List.map (fun s > match s with Eq eq > eq  _ > assert false) c.stmts

840

in

841

let undefined_vars_init =

842

List.fold_left (fun uvs v > ISet.add v.var_id uvs) ISet.empty c.locals

843

in

844

let _ =

845

List.fold_left

846

(type_eq (env, vd_env) false (*is_main*))

847

undefined_vars_init eqs

848

in

849

(* Typing each predicate expr *)

850

let type_pred_ee ee : unit =

851

type_subtyping_arg (env, vd_env) false (* not in main *) false

852

(* not a const *)

853

ee.eexpr_qfexpr type_bool

854

in

855

List.iter type_pred_ee

856

(c.assume @ c.guarantees

857

@ List.flatten (List.map (fun m > m.ensure @ m.require) c.modes));

858

(*TODO enrich env locally with locals and consts type each pre/post as a

859

boolean expr I don't know if we want to update the global env with locally

860

typed variables. For the moment, returning the provided env *)

861

env

862


863

let rec type_spec env spec =

864

match spec with Contract c > type_contract env c  NodeSpec _ > env

865


866

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

867

used for error reports. *)

868

and type_node env nd loc =

869

(* Format.eprintf "Typing node %s@." nd.node_id; *)

870

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

871

(* In contracts, outputs are considered as input values *)

872

let vd_env_ol =

873

if nd.node_iscontract then nd.node_locals

874

else nd.node_outputs @ nd.node_locals

875

in

876

let vd_env = nd.node_inputs @ nd.node_outputs @ nd.node_locals in

877

check_vd_env vd_env;

878

let init_env = env in

879

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

880

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

881

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

882

let new_env = Env.overwrite env delta_env in

883

let undefined_vars_init =

884

List.fold_left (fun uvs v > ISet.add v.var_id uvs) ISet.empty vd_env_ol

885

in

886

let undefined_vars =

887

let eqs, _ = get_node_eqs nd in

888

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

889

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

890

in

891

(* Typing asserts *)

892

List.iter

893

(fun assert_ >

894

let assert_expr = assert_.assert_expr in

895

type_subtyping_arg (new_env, vd_env) is_main false assert_expr

896

(* Type_predef. *)

897

type_bool)

898

nd.node_asserts;

899

(* Typing spec/contracts *)

900

(match nd.node_spec with

901

 None >

902

()

903

 Some spec >

904

ignore (type_spec new_env spec));

905

(* Typing annots *)

906

List.iter

907

(fun annot >

908

List.iter

909

(fun (_, eexpr) > ignore (type_eexpr (new_env, vd_env) eexpr))

910

annot.annots)

911

nd.node_annot;

912


913

(* check that table is empty *)

914

let local_consts =

915

List.fold_left

916

(fun res vdecl >

917

if vdecl.var_dec_const then ISet.add vdecl.var_id res else res)

918

ISet.empty nd.node_locals

919

in

920

let undefined_vars = ISet.diff undefined_vars local_consts in

921


922

if not (ISet.is_empty undefined_vars) then

923

raise (Error (loc, Undefined_var undefined_vars));

924

let ty_ins = type_of_vlist nd.node_inputs in

925

let ty_outs = type_of_vlist nd.node_outputs in

926

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

927

generalize ty_node;

928

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

929

nd.node_type < Expr_type_hub.export ty_node;

930

Env.add_value env nd.node_id ty_node

931


932

let type_imported_node env nd _loc =

933

let vd_env = nd.nodei_inputs @ nd.nodei_outputs in

934

check_vd_env vd_env;

935

let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in

936

let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in

937

let new_env = Env.overwrite env delta_env in

938

(* Typing spec *)

939

(match nd.nodei_spec with

940

 None >

941

()

942

 Some spec >

943

ignore (type_spec new_env spec));

944

let ty_ins = type_of_vlist nd.nodei_inputs in

945

let ty_outs = type_of_vlist nd.nodei_outputs in

946

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

947

generalize ty_node;

948

(* if (is_polymorphic ty_node) then raise (Error (loc, Poly_imported_node

949

nd.nodei_id)); *)

950

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

951

nd.nodei_type < Expr_type_hub.export ty_node;

952

new_env

953


954

let type_top_const env cdecl =

955

let ty = type_const cdecl.const_loc cdecl.const_value in

956

let d =

957

if is_dimension_type ty then

958

dimension_of_const cdecl.const_loc cdecl.const_value

959

else Dimension.mkdim_var ()

960

in

961

let ty =

962

(* Type_predef. *)

963

type_static d ty

964

in

965

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

966

cdecl.const_type < Expr_type_hub.export ty;

967

new_env

968


969

let type_top_consts env clist = List.fold_left type_top_const env clist

970


971

let rec type_top_decl env decl =

972

match decl.top_decl_desc with

973

 Node nd > (

974

try type_node env nd decl.top_decl_loc

975

with Error _ as exc >

976

if !Options.global_inline then

977

Format.eprintf "Type error: failing node@.%a@.@?" Printers.pp_node nd;

978

raise exc)

979

 ImportedNode nd >

980

type_imported_node env nd decl.top_decl_loc

981

 Const c >

982

type_top_const env c

983

 TypeDef _ >

984

List.fold_left type_top_decl env (consts_of_enum_type decl)

985

 Include _  Open _ >

986

env

987


988

let get_type_of_call decl =

989

match decl.top_decl_desc with

990

 Node nd >

991

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

992

type_list_of_type in_typ, type_list_of_type out_typ

993

 ImportedNode nd >

994

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

995

type_list_of_type in_typ, type_list_of_type out_typ

996

 _ >

997

assert false

998


999

let type_prog env decls =

1000

try List.fold_left type_top_decl env decls

1001

with Failure _ as exc > raise exc

1002


1003

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

1004

description of dimensions, with constant parameters, instead of unifiable

1005

internal variables. *)

1006


1007

(* The following functions aims at 'unevaluating' dimension expressions

1008

occuring in array types, i.e. replacing unifiable second_order variables

1009

with the original static parameters. Once restored in this formulation,

1010

dimensions may be meaningfully printed. *)

1011

let uneval_vdecl_generics vdecl =

1012

if vdecl.var_dec_const then

1013

match get_static_value (Expr_type_hub.import vdecl.var_type) with

1014

 None >

1015

Format.eprintf "internal error: %a@." (* Types. *) print_ty

1016

(Expr_type_hub.import vdecl.var_type);

1017

assert false

1018

 Some d >

1019

Dimension.uneval vdecl.var_id d

1020


1021

let uneval_node_generics vdecls = List.iter uneval_vdecl_generics vdecls

1022


1023

let uneval_spec_generics spec =

1024

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

1025


1026

let uneval_top_generics decl =

1027

match decl.top_decl_desc with

1028

 Node nd >

1029

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

1030

 ImportedNode nd >

1031

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

1032

 Const _  TypeDef _  Open _  Include _ >

1033

()

1034


1035

let uneval_prog_generics prog = List.iter uneval_top_generics prog

1036


1037

let rec get_imported_symbol decls id =

1038

match decls with

1039

 [] >

1040

assert false

1041

 decl :: q > (

1042

match decl.top_decl_desc with

1043

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

1044

decl

1045

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

1046

decl

1047

 TypeDef _ >

1048

get_imported_symbol (consts_of_enum_type decl @ q) id

1049

 _ >

1050

get_imported_symbol q id)

1051


1052

let check_env_compat header declared computed =

1053

uneval_prog_generics header;

1054

Env.iter declared (fun k decl_type_k >

1055

let top = get_imported_symbol header k in

1056

let loc = top.top_decl_loc in

1057

try

1058

let computed_t = Env.lookup_value computed k in

1059

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

1060

(* Types.print_ty Format.std_formatter decl_type_k; Types.print_ty

1061

Format.std_formatter computed_t;*)

1062

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

1063

with Not_found > (

1064

(* If top is a contract we do not require the lustre file to provide

1065

the same definition. *)

1066

match top.top_decl_desc with

1067

 Node nd > (

1068

match nd.node_spec with

1069

 Some (Contract _) >

1070

()

1071

 _ >

1072

raise (Error (loc, Declared_but_undefined k)))

1073

 _ >

1074

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

1075


1076

let check_typedef_top decl =

1077

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

1078

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

1079

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

1080

match decl.top_decl_desc with

1081

 TypeDef ty > (

1082

let owner = decl.top_decl_owner in

1083

let itf = decl.top_decl_itf in

1084

let decl' =

1085

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

1086

with Not_found >

1087

raise

1088

(Error

1089

( decl.top_decl_loc,

1090

Declared_but_undefined ("type " ^ ty.tydef_id) ))

1091

in

1092

let owner' = decl'.top_decl_owner in

1093

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

1094

let itf' = decl'.top_decl_itf in

1095

match decl'.top_decl_desc with

1096

 Const _  Node _  ImportedNode _ >

1097

assert false

1098

 TypeDef ty'

1099

when coretype_equal ty'.tydef_desc ty.tydef_desc

1100

&& owner' = owner && itf && not itf' >

1101

()

1102

 _ >

1103

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

1104

 _ >

1105

()

1106


1107

let check_typedef_compat header = List.iter check_typedef_top header

1108

end

1109


1110

include

1111

Make

1112

(Types.Main)

1113

(struct

1114

type type_expr = Types.Main.type_expr

1115


1116

let import x = x

1117


1118

let export x = x

1119

end)

1120

(* Local Variables: *)

1121

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

1122

(* End: *)
