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

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

18

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

19

redefinition allowed. *)

20


21

open Utils

22


23

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

24

yet this makes notations far lighter.*)

25

open Lustre_types

26

open Corelang

27


28

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

29

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

30

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

31


32

module type EXPR_TYPE_HUB = sig

33

type type_expr

34


35

val import : Types.t > type_expr

36


37

val export : type_expr > Types.t

38

end

39


40

module Make

41

(T : Types.S)

42

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

43

struct

44

module TP = Type_predef.Make (T)

45

include TP

46


47

(* XXX: UNUSED *)

48

(* let pp_typing_env fmt env = Env.pp print_ty fmt env *)

49


50

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

51

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

52

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

53


54

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

55

[ty]. False otherwise. *)

56

let rec occurs tvar ty =

57

let ty = repr ty in

58

match type_desc ty with

59

 Tvar >

60

ty = tvar

61

 Tarrow (t1, t2) >

62

occurs tvar t1  occurs tvar t2

63

 Ttuple tl >

64

List.exists (occurs tvar) tl

65

 Tstruct fl >

66

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

67

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

68

occurs tvar t

69

 Tenum _  Tconst _  Tunivar  Tbasic _ >

70

false

71


72

(* Generalize by sideeffects *)

73


74

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

75

let rec generalize ty =

76

match type_desc ty with

77

 Tvar >

78

(* No scopes, always generalize *)

79

ty.tdesc < Tunivar

80

 Tarrow (t1, t2) >

81

generalize t1;

82

generalize t2

83

 Ttuple tl >

84

List.iter generalize tl

85

 Tstruct fl >

86

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

87

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

88

Dimension.generalize d;

89

generalize t

90

 Tclock t  Tlink t >

91

generalize t

92

 Tenum _  Tconst _  Tunivar  Tbasic _ >

93

()

94


95

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

96

let rec instantiate inst_vars inst_dim_vars ty =

97

let ty = repr ty in

98

match ty.tdesc with

99

 Tenum _  Tconst _  Tvar  Tbasic _ >

100

ty

101

 Tarrow (t1, t2) >

102

{

103

ty with

104

tdesc =

105

Tarrow

106

( instantiate inst_vars inst_dim_vars t1,

107

instantiate inst_vars inst_dim_vars t2 );

108

}

109

 Ttuple tlist >

110

{

111

ty with

112

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

113

}

114

 Tstruct flist >

115

{

116

ty with

117

tdesc =

118

Tstruct

119

(List.map

120

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

121

flist);

122

}

123

 Tclock t >

124

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

125

 Tstatic (d, t) >

126

{

127

ty with

128

tdesc =

129

Tstatic

130

( Dimension.instantiate inst_dim_vars d,

131

instantiate inst_vars inst_dim_vars t );

132

}

133

 Tarray (d, t) >

134

{

135

ty with

136

tdesc =

137

Tarray

138

( Dimension.instantiate inst_dim_vars d,

139

instantiate inst_vars inst_dim_vars t );

140

}

141

 Tlink t >

142

(* should not happen *)

143

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

144

 Tunivar > (

145

try List.assoc ty.tid !inst_vars

146

with Not_found >

147

let var = new_var () in

148

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

149

var)

150


151

let basic_coretype_type t =

152

if is_real_type t then Tydec_real

153

else if is_int_type t then Tydec_int

154

else if is_bool_type t then Tydec_bool

155

else assert false

156


157

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

158

let rec type_coretype type_dim cty =

159

match (*get_repr_type*)

160

cty with

161

 Tydec_any >

162

new_var ()

163

 Tydec_int >

164

type_int

165

 Tydec_real >

166

(* Type_predef. *)

167

type_real

168

(*  Tydec_float > Type_predef.type_real *)

169

 Tydec_bool >

170

(* Type_predef. *)

171

type_bool

172

 Tydec_clock ty >

173

(* Type_predef. *)

174

type_clock (type_coretype type_dim ty)

175

 Tydec_const c >

176

(* Type_predef. *)

177

type_const c

178

 Tydec_enum tl >

179

(* Type_predef. *)

180

type_enum tl

181

 Tydec_struct fl >

182

(* Type_predef. *)

183

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

184

 Tydec_array (d, ty) >

185

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

186

type_dim d;

187

(* Type_predef. *)

188

type_array d (type_coretype type_dim ty)

189


190

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

191

let rec coretype_type ty =

192

match (repr ty).tdesc with

193

 Tvar >

194

Tydec_any

195

 Tbasic _ >

196

basic_coretype_type ty

197

 Tconst c >

198

Tydec_const c

199

 Tclock t >

200

Tydec_clock (coretype_type t)

201

 Tenum tl >

202

Tydec_enum tl

203

 Tstruct fl >

204

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

205

 Tarray (d, t) >

206

Tydec_array (d, coretype_type t)

207

 Tstatic (_, t) >

208

coretype_type t

209

 _ >

210

assert false

211


212

let get_coretype_definition tname =

213

try

214

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

215

match top.top_decl_desc with

216

 TypeDef tdef >

217

tdef.tydef_desc

218

 _ >

219

assert false

220

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

221


222

let get_type_definition tname =

223

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

224


225

(* Equality on ground types only *)

226

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

227

let rec eq_ground t1 t2 =

228

let t1 = repr t1 in

229

let t2 = repr t2 in

230

t1 == t2

231



232

match t1.tdesc, t2.tdesc with

233

 Tbasic t1, Tbasic t2 when t1 == t2 >

234

true

235

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

236

true

237

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

238

List.for_all2 eq_ground tl tl'

239

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

240

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

241

 Tconst t, _ >

242

let def_t = get_type_definition t in

243

eq_ground def_t t2

244

 _, Tconst t >

245

let def_t = get_type_definition t in

246

eq_ground t1 def_t

247

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

248

eq_ground t1 t1' && eq_ground t2 t2'

249

 Tclock t1', Tclock t2' >

250

eq_ground t1' t2'

251

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

252

>

253

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

254

 _ >

255

false

256


257

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

258

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

259

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

260

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

261

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

262

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

263

and constants are handled differently.*)

264

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

265

let rec unif t1 t2 =

266

let t1 = repr t1 in

267

let t2 = repr t2 in

268

if t1 == t2 then ()

269

else

270

match t1.tdesc, t2.tdesc with

271

(* strictly subtyping cases first *)

272

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

273

unif t1 t2

274

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

275

unif t1 t2

276

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

277

 Tvar, Tvar >

278

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

279

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

280

t1.tdesc < Tlink t2

281

 _, Tvar when not (occurs t2 t1) >

282

t2.tdesc < Tlink t1

283

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

284

unif t2 t2';

285

unif t1' t1

286

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

287

List.iter2 unif tl tl'

288

 Ttuple [ t1 ], _ >

289

unif t1 t2

290

 _, Ttuple [ t2 ] >

291

unif t1 t2

292

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

293

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

294

 Tclock _, Tstatic _  Tstatic _, Tclock _ >

295

raise (Unify (t1, t2))

296

 Tclock t1', Tclock t2' >

297

unif t1' t2'

298

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

299

 Tunivar, _  _, Tunivar >

300

()

301

 Tconst t, _ >

302

let def_t = get_type_definition t in

303

unif def_t t2

304

 _, Tconst t >

305

let def_t = get_type_definition t in

306

unif t1 def_t

307

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

308

()

309

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

310

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

311

let eval_const =

312

if semi then fun c > Some (Dimension.mkdim_ident Location.dummy c)

313

else fun _ > None

314

in

315

unif t1' t2';

316

Dimension.eval Basic_library.eval_dim_env eval_const e1;

317

Dimension.eval Basic_library.eval_dim_env eval_const e2;

318

Dimension.unify ~semi e1 e2

319

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

320

for numerical constants with non static ones for variables with

321

possible machine types *)

322

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

323

BasicT.unify bt1 bt2

324

 _, _ >

325

raise (Unify (t1, t2))

326

in

327

unif t1 t2

328


329

(* Expected type ty1, got type ty2 *)

330

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

331

try unify ~sub ~semi ty1 ty2 with

332

 Unify _ >

333

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

334

 Dimension.Unify _ >

335

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

336


337

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

338

(* Typing function for each basic AST construct *)

339

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

340


341

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

342

if Hashtbl.mem field_table label then (

343

let tydef = Hashtbl.find field_table label in

344

let tydec = (typedef_of_top tydef).tydef_desc in

345

let tydec_struct = get_struct_type_fields tydec in

346

let ty_label =

347

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

348

in

349

try_unify ty_label (type_const ~is_annot loc c) loc;

350

type_coretype (fun _ > ()) tydec)

351

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

352


353

and type_const ?(is_annot = false) loc c =

354

match c with

355

 Const_int _ >

356

(* Type_predef. *)

357

type_int

358

 Const_real _ >

359

(* Type_predef. *)

360

type_real

361

 Const_array ca >

362

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

363

let ty = new_var () in

364

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

365

(* Type_predef. *)

366

type_array d ty

367

 Const_tag t >

368

if Hashtbl.mem tag_table t then

369

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

370

let tydec =

371

if is_user_type tydef.tydef_desc then Tydec_const tydef.tydef_id

372

else tydef.tydef_desc

373

in

374

type_coretype (fun _ > ()) tydec

375

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

376

 Const_struct fl > (

377

let ty_struct = new_var () in

378

let used =

379

List.fold_left

380

(fun acc (l, c) >

381

if List.mem l acc then

382

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

383

else

384

try_unify

385

ty_struct

386

(type_struct_const_field ~is_annot loc (l, c))

387

loc;

388

l :: acc)

389

[]

390

fl

391

in

392

try

393

let total =

394

List.map fst (get_struct_type_fields (coretype_type ty_struct))

395

in

396

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

397

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

398

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

399

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

400

with Not_found > ty_struct)

401

 Const_string s  Const_modeid s >

402

if is_annot then (* Type_predef. *)

403

type_string

404

else (

405

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

406

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

407


408

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

409

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

410

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

411

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

412

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

413

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

414

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

415

the typing process. *)

416

let check_constant loc const_expected const_real =

417

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

418


419

let rec type_add_const env const arg targ =

420

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

421

Types.pp targ;*)

422

if const then (

423

let d =

424

if is_dimension_type targ then dimension_of_expr arg

425

else Dimension.mkdim_var ()

426

in

427

let eval_const id =

428

(* Types. *)

429

get_static_value (Env.lookup_value (fst env) id)

430

in

431

Dimension.eval Basic_library.eval_dim_env eval_const d;

432

let real_static_type =

433

(* Type_predef. *)

434

type_static d ((* Types. *)

435

dynamic_type targ)

436

in

437

(match (* Types. *)

438

get_static_value targ with

439

 None >

440

()

441

 Some _ >

442

try_unify targ real_static_type arg.expr_loc);

443

real_static_type)

444

else targ

445


446

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

447

applications and assignments *)

448

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

449

let loc = real_arg.expr_loc in

450

let const =

451

const

452

 (* Types. *)

453

get_static_value formal_type <> None

454

in

455

let real_type =

456

type_add_const env const real_arg (type_expr env in_main const real_arg)

457

in

458

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

459

Printers.pp_expr real_arg Types.pp real_type Types.pp formal_type;*)

460

try_unify ~sub formal_type real_type loc

461


462

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

463

match real const (maybe symbolic) arguments  checking type adequation

464

between formal and real arguments An application may embed an

465

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

466

calls *)

467

and type_appl env in_main loc const f args =

468

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

469

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

470

then

471

try

472

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

473

(* Types. *)

474

type_of_type_list

475

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

476

with Utils.TransposeError (l, l') >

477

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

478

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

479


480

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

481

(argument, type) pairs. *)

482

and type_dependent_call env in_main loc const f targs =

483

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

484

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

485

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

486

let tfun =

487

(* Type_predef. *)

488

type_arrow tins touts

489

in

490

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

491

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

492

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

493

let tins = type_list_of_type tins in

494

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

495

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

496

else (

497

List.iter2

498

(fun (a, t) ti >

499

let t' =

500

type_add_const

501

env

502

(const

503

 (* Types. *)

504

get_static_value ti <> None)

505

a

506

t

507

in

508

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

509

touts; *)

510

try_unify ~sub:true ti t' a.expr_loc

511

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

512

touts; *))

513

targs

514

tins;

515

touts)

516


517

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

518

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

519

and type_simple_call env in_main loc const f targs =

520

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

521

let tfun =

522

(* Type_predef. *)

523

type_arrow tins touts

524

in

525

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

526

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

527

(type_of_type_list targs);*)

528

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

529

touts

530


531

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

532

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

533

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

534

let resulting_ty =

535

match expr.expr_desc with

536

 Expr_const c >

537

let ty = type_const ~is_annot expr.expr_loc c in

538

let ty =

539

(* Type_predef. *)

540

type_static (Dimension.mkdim_var ()) ty

541

in

542

expr.expr_type < Expr_type_hub.export ty;

543

ty

544

 Expr_ident v >

545

let tyv =

546

try Env.lookup_value (fst env) v

547

with Not_found >

548

Format.eprintf

549

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

550

Printers.pp_expr

551

expr;

552

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

553

in

554

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

555

let ty' =

556

if const then

557

(* Type_predef. *)

558

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

559

else new_var ()

560

in

561

try_unify ty ty' expr.expr_loc;

562

expr.expr_type < Expr_type_hub.export ty;

563

ty

564

 Expr_array elist >

565

let ty_elt = new_var () in

566

List.iter

567

(fun e >

568

try_unify

569

ty_elt

570

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

571

e.expr_loc)

572

elist;

573

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

574

let ty =

575

(* Type_predef. *)

576

type_array d ty_elt

577

in

578

expr.expr_type < Expr_type_hub.export ty;

579

ty

580

 Expr_access (e1, d) >

581

type_subtyping_arg

582

env

583

in_main

584

false

585

(* not necessary a constant *)

586

(expr_of_dimension d)

587

(* Type_predef. *)

588

type_int;

589

let ty_elt = new_var () in

590

let d = Dimension.mkdim_var () in

591

type_subtyping_arg

592

env

593

in_main

594

const

595

e1

596

((* Type_predef. *)

597

type_array d ty_elt);

598

expr.expr_type < Expr_type_hub.export ty_elt;

599

ty_elt

600

 Expr_power (e1, d) >

601

let eval_const id =

602

(* Types. *)

603

get_static_value (Env.lookup_value (fst env) id)

604

in

605

type_subtyping_arg

606

env

607

in_main

608

true

609

(expr_of_dimension d)

610

(* Type_predef. *)

611

type_int;

612

Dimension.eval Basic_library.eval_dim_env eval_const d;

613

let ty_elt =

614

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

615

in

616

let ty =

617

(* Type_predef. *)

618

type_array d ty_elt

619

in

620

expr.expr_type < Expr_type_hub.export ty;

621

ty

622

 Expr_tuple elist >

623

let ty =

624

new_ty

625

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

626

in

627

expr.expr_type < Expr_type_hub.export ty;

628

ty

629

 Expr_ite (c, t, e) >

630

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

631

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

632

expr.expr_type < Expr_type_hub.export ty;

633

ty

634

 Expr_appl (id, args, r) >

635

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

636

expression *)

637

(match r with

638

 None >

639

()

640

 Some c >

641

check_constant expr.expr_loc const false;

642

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

643

let args_list = expr_list_of_expr args in

644

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

645

let targs =

646

new_ty

647

(match args_list with

648

 [a] > (Expr_type_hub.import a.expr_type).tdesc

649

 _ >

650

Ttuple

651

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

652

in

653

args.expr_type < Expr_type_hub.export targs;

654

expr.expr_type < Expr_type_hub.export touts;

655

touts

656

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

657

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

658

check_constant expr.expr_loc const false;

659

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

660

expr.expr_type < Expr_type_hub.export ty;

661

ty

662

 Expr_pre e >

663

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

664

check_constant expr.expr_loc const false;

665

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

666

expr.expr_type < Expr_type_hub.export ty;

667

ty

668

 Expr_when (e1, c, l) >

669

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

670

check_constant expr.expr_loc const false;

671

let typ_l =

672

(* Type_predef. *)

673

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

674

in

675

let expr_c = expr_of_ident c expr.expr_loc in

676

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

677

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

678

expr.expr_type < Expr_type_hub.export ty;

679

ty

680

 Expr_merge (c, hl) >

681

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

682

check_constant expr.expr_loc const false;

683

let typ_in, typ_out =

684

type_branches env in_main expr.expr_loc const hl

685

in

686

let expr_c = expr_of_ident c expr.expr_loc in

687

let typ_l =

688

(* Type_predef. *)

689

type_clock typ_in

690

in

691

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

692

expr.expr_type < Expr_type_hub.export typ_out;

693

typ_out

694

in

695

Log.report ~level:3 (fun fmt >

696

Format.fprintf

697

fmt

698

"Type of expr %a: %a@ "

699

Printers.pp_expr

700

expr

701

(* Types. *)

702

pp

703

resulting_ty);

704

resulting_ty

705


706

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

707

let typ_in = new_var () in

708

let typ_out = new_var () in

709

try

710

let used_labels =

711

List.fold_left

712

(fun accu (t, h) >

713

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

714

type_subtyping_arg env in_main const h typ_out;

715

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

716

else t :: accu)

717

[]

718

hl

719

in

720

let type_labels = get_enum_type_tags (coretype_type typ_in) in

721

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

722

let unbound_tag =

723

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

724

in

725

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

726

else typ_in, typ_out

727

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

728


729

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

730

env *)

731

let type_eexpr env eexpr =

732

type_expr

733

~is_annot:true

734

env

735

false

736

(* not in main *) false (* not a const *)

737

eexpr.eexpr_qfexpr

738


739

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

740

let type_eq env in_main undefined_vars eq =

741

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

742

(* Check undefined variables, type lhs *)

743

let expr_lhs =

744

expr_of_expr_list

745

eq.eq_loc

746

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

747

in

748

let ty_lhs = type_expr env in_main false expr_lhs in

749

(* Check multiple variable definitions *)

750

let define_var id uvars =

751

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

752

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

753

in

754

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

755

let ty_lhs =

756

type_of_type_list

757

(List.map2

758

(fun ty id >

759

if get_static_value ty <> None then

760

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

761

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

762

(type_list_of_type ty_lhs)

763

eq.eq_lhs)

764

in

765

let undefined_vars =

766

List.fold_left

767

(fun uvars v > define_var v uvars)

768

undefined_vars

769

eq.eq_lhs

770

in

771

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

772

assigned to a (always nonconstant) lhs variable *)

773

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

774

undefined_vars

775


776

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

777

environment [env] *)

778

let type_coreclock env ck id loc =

779

match ck.ck_dec_desc with

780

 Ckdec_any >

781

()

782

 Ckdec_bool cl >

783

let dummy_id_expr = expr_of_ident id loc in

784

let when_expr =

785

List.fold_left

786

(fun expr (x, l) >

787

{

788

expr_tag = new_tag ();

789

expr_desc = Expr_when (expr, x, l);

790

expr_type = Types.new_var ();

791

expr_clock = Clocks.new_var true;

792

expr_delay = Delay.new_var ();

793

expr_loc = loc;

794

expr_annot = None;

795

})

796

dummy_id_expr

797

cl

798

in

799

ignore (type_expr env false false when_expr)

800


801

let rec check_type_declaration loc cty =

802

match cty with

803

 Tydec_clock ty  Tydec_array (_, ty) >

804

check_type_declaration loc ty

805

 Tydec_const tname >

806

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

807

if not (Hashtbl.mem type_table cty) then

808

raise (Error (loc, Unbound_type tname))

809

 _ >

810

()

811


812

let type_var_decl vd_env env vdecl =

813

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

814

Printers.pp_dec_ty vdecl.var_dec_type.ty_dec_desc;*)

815

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

816

let eval_const id =

817

(* Types. *)

818

get_static_value (Env.lookup_value env id)

819

in

820

let type_dim d =

821

type_subtyping_arg

822

(env, vd_env)

823

false

824

true

825

(expr_of_dimension d)

826

(* Type_predef. *)

827

type_int;

828

Dimension.eval Basic_library.eval_dim_env eval_const d

829

in

830

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

831


832

let ty_static =

833

if vdecl.var_dec_const then

834

(* Type_predef. *)

835

type_static (Dimension.mkdim_var ()) ty

836

else ty

837

in

838

(match vdecl.var_dec_value with

839

 None >

840

()

841

 Some v >

842

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

843

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

844

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

845

type_coreclock

846

(new_env, vd_env)

847

vdecl.var_dec_clock

848

vdecl.var_id

849

vdecl.var_loc;

850

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

851

new_env

852


853

let type_var_decl_list vd_env env l =

854

List.fold_left (type_var_decl vd_env) env l

855


856

let type_of_vlist vars =

857

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

858

type_of_type_list tyl

859


860

let add_vdecl vd_env vdecl =

861

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

862

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

863

else vdecl :: vd_env

864


865

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

866


867

let type_contract env c =

868

let vd_env = c.consts @ c.locals in

869

check_vd_env vd_env;

870

let env =

871

type_var_decl_list

872

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

873

vd_env

874

env

875

vd_env

876

in

877

(* typing stmts *)

878

let eqs =

879

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

880

in

881

let undefined_vars_init =

882

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

883

in

884

let _ =

885

List.fold_left

886

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

887

undefined_vars_init

888

eqs

889

in

890

(* Typing each predicate expr *)

891

let type_pred_ee ee : unit =

892

type_subtyping_arg

893

(env, vd_env)

894

false

895

(* not in main *) false

896

(* not a const *)

897

ee.eexpr_qfexpr

898

type_bool

899

in

900

List.iter

901

type_pred_ee

902

(c.assume @ c.guarantees

903

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

904

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

905

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

906

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

907

env

908


909

let rec type_spec env spec =

910

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

911


912

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

913

used for error reports. *)

914

and type_node env nd loc =

915

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

916

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

917

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

918

let vd_env_ol =

919

if nd.node_iscontract then nd.node_locals

920

else nd.node_outputs @ nd.node_locals

921

in

922

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

923

check_vd_env vd_env;

924

let init_env = env in

925

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

926

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

927

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

928

let new_env = Env.overwrite env delta_env in

929

let undefined_vars_init =

930

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

931

in

932

let undefined_vars =

933

let eqs, _ = get_node_eqs nd in

934

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

935

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

936

in

937

(* Typing asserts *)

938

List.iter

939

(fun assert_ >

940

let assert_expr = assert_.assert_expr in

941

type_subtyping_arg

942

(new_env, vd_env)

943

is_main

944

false

945

assert_expr

946

(* Type_predef. *)

947

type_bool)

948

nd.node_asserts;

949

(* Typing spec/contracts *)

950

(match nd.node_spec with

951

 None >

952

()

953

 Some spec >

954

ignore (type_spec new_env spec));

955

(* Typing annots *)

956

List.iter

957

(fun annot >

958

List.iter

959

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

960

annot.annots)

961

nd.node_annot;

962


963

(* check that table is empty *)

964

let local_consts =

965

List.fold_left

966

(fun res vdecl >

967

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

968

ISet.empty

969

nd.node_locals

970

in

971

let undefined_vars = ISet.diff undefined_vars local_consts in

972


973

if not (ISet.is_empty undefined_vars) then

974

raise (Error (loc, Undefined_var undefined_vars));

975

let ty_ins = type_of_vlist nd.node_inputs in

976

let ty_outs = type_of_vlist nd.node_outputs in

977

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

978

generalize ty_node;

979

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

980

nd.node_type < Expr_type_hub.export ty_node;

981

Env.add_value env nd.node_id ty_node

982


983

let type_imported_node env nd _loc =

984

let vd_env = nd.nodei_inputs @ nd.nodei_outputs in

985

check_vd_env vd_env;

986

let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in

987

let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in

988

let new_env = Env.overwrite env delta_env in

989

(* Typing spec *)

990

(match nd.nodei_spec with

991

 None >

992

()

993

 Some spec >

994

ignore (type_spec new_env spec));

995

let ty_ins = type_of_vlist nd.nodei_inputs in

996

let ty_outs = type_of_vlist nd.nodei_outputs in

997

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

998

generalize ty_node;

999

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

1000

nd.nodei_id)); *)

1001

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

1002

nd.nodei_type < Expr_type_hub.export ty_node;

1003

new_env

1004


1005

let type_top_const env cdecl =

1006

let ty = type_const cdecl.const_loc cdecl.const_value in

1007

let d =

1008

if is_dimension_type ty then

1009

dimension_of_const cdecl.const_loc cdecl.const_value

1010

else Dimension.mkdim_var ()

1011

in

1012

let ty =

1013

(* Type_predef. *)

1014

type_static d ty

1015

in

1016

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

1017

cdecl.const_type < Expr_type_hub.export ty;

1018

new_env

1019


1020

(* XXX: UNUSED *)

1021

(* let type_top_consts env clist = List.fold_left type_top_const env clist *)

1022


1023

let rec type_top_decl env decl =

1024

match decl.top_decl_desc with

1025

 Node nd > (

1026

try type_node env nd decl.top_decl_loc

1027

with Error _ as exc >

1028

if !Options.global_inline then

1029

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

1030

raise exc)

1031

 ImportedNode nd >

1032

type_imported_node env nd decl.top_decl_loc

1033

 Const c >

1034

type_top_const env c

1035

 TypeDef _ >

1036

List.fold_left type_top_decl env (consts_of_enum_type decl)

1037

 Include _  Open _ >

1038

env

1039


1040

(* XXX: UNUSED *)

1041

(* let get_type_of_call decl =

1042

* match decl.top_decl_desc with

1043

*  Node nd >

1044

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

1045

* type_list_of_type in_typ, type_list_of_type out_typ

1046

*  ImportedNode nd >

1047

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

1048

* type_list_of_type in_typ, type_list_of_type out_typ

1049

*  _ >

1050

* assert false *)

1051


1052

let type_prog env decls =

1053

(* try *)

1054

List.fold_left type_top_decl env decls

1055

(* with Failure _ as exc > raise exc *)

1056


1057

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

1058

description of dimensions, with constant parameters, instead of unifiable

1059

internal variables. *)

1060


1061

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

1062

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

1063

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

1064

dimensions may be meaningfully printed. *)

1065

let uneval_vdecl_generics vdecl =

1066

if vdecl.var_dec_const then

1067

match get_static_value (Expr_type_hub.import vdecl.var_type) with

1068

 None >

1069

Format.eprintf

1070

"internal error: %a@."

1071

(* Types. *) pp

1072

(Expr_type_hub.import vdecl.var_type);

1073

assert false

1074

 Some d >

1075

Dimension.uneval vdecl.var_id d

1076


1077

let uneval_node_generics vdecls = List.iter uneval_vdecl_generics vdecls

1078


1079

(* XXX: UNUSED *)

1080

(* let uneval_spec_generics spec =

1081

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

1082


1083

let uneval_top_generics decl =

1084

match decl.top_decl_desc with

1085

 Node nd >

1086

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

1087

 ImportedNode nd >

1088

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

1089

 Const _  TypeDef _  Open _  Include _ >

1090

()

1091


1092

let uneval_prog_generics prog = List.iter uneval_top_generics prog

1093


1094

let rec get_imported_symbol decls id =

1095

match decls with

1096

 [] >

1097

assert false

1098

 decl :: q > (

1099

match decl.top_decl_desc with

1100

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

1101

decl

1102

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

1103

decl

1104

 TypeDef _ >

1105

get_imported_symbol (consts_of_enum_type decl @ q) id

1106

 _ >

1107

get_imported_symbol q id)

1108


1109

let check_env_compat header declared computed =

1110

uneval_prog_generics header;

1111

Env.iter declared (fun k decl_type_k >

1112

let top = get_imported_symbol header k in

1113

let loc = top.top_decl_loc in

1114

try

1115

let computed_t = Env.lookup_value computed k in

1116

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

1117

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

1118

Format.std_formatter computed_t;*)

1119

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

1120

with Not_found > (

1121

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

1122

the same definition. *)

1123

match top.top_decl_desc with

1124

 Node nd > (

1125

match nd.node_spec with

1126

 Some (Contract _) >

1127

()

1128

 _ >

1129

raise (Error (loc, Declared_but_undefined k)))

1130

 _ >

1131

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

1132


1133

let check_typedef_top decl =

1134

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

1135

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

1136

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

1137

match decl.top_decl_desc with

1138

 TypeDef ty > (

1139

let owner = decl.top_decl_owner in

1140

let itf = decl.top_decl_itf in

1141

let decl' =

1142

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

1143

with Not_found >

1144

raise

1145

(Error

1146

( decl.top_decl_loc,

1147

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

1148

in

1149

let owner' = decl'.top_decl_owner in

1150

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

1151

let itf' = decl'.top_decl_itf in

1152

match decl'.top_decl_desc with

1153

 Const _  Node _  ImportedNode _ >

1154

assert false

1155

 TypeDef ty'

1156

when coretype_equal ty'.tydef_desc ty.tydef_desc

1157

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

1158

()

1159

 _ >

1160

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

1161

 _ >

1162

()

1163


1164

let check_typedef_compat header = List.iter check_typedef_top header

1165

end

1166


1167

module Expr_type_hub : EXPR_TYPE_HUB with type type_expr = Types.t = struct

1168

type type_expr = Types.t

1169


1170

let import x = x

1171


1172

let export x = x

1173

end

1174


1175

include Make (Types) (Expr_type_hub)

1176


1177

(* Local Variables: *)

1178

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

1179

(* End: *)
