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

open Utils

15

(** Types definitions and a few utility functions on types. *)

16


17

module type BASIC_TYPES = sig

18

type t

19


20

val pp : Format.formatter > t > unit

21


22

val pp_c : Format.formatter > t > unit

23


24

val is_scalar_type : t > bool

25


26

val is_numeric_type : t > bool

27


28

val is_int_type : t > bool

29


30

val is_real_type : t > bool

31


32

val is_bool_type : t > bool

33


34

val is_dimension_type : t > bool

35


36

val type_int_builder : t

37


38

val type_real_builder : t

39


40

val type_bool_builder : t

41


42

val type_string_builder : t

43


44

val unify : t > t > unit

45


46

val is_unifiable : t > t > bool

47

end

48


49

module type S = sig

50

module BasicT : BASIC_TYPES

51


52

type basic_type = BasicT.t

53


54

type t = { mutable tdesc : type_desc; tid : int }

55


56

and type_desc =

57

 Tconst of ident

58

(* type constant *)

59

 Tbasic of basic_type

60

 Tclock of t

61

(* A type expression explicitely tagged as carrying a clock *)

62

 Tarrow of t * t

63

 Ttuple of t list

64

 Tenum of ident list

65

 Tstruct of (ident * t) list

66

 Tarray of Dimension.t * t

67

 Tstatic of Dimension.t * t

68

(* a type carried by a dimension expression *)

69

 Tlink of t

70

(* During unification, make links instead of substitutions *)

71

 Tvar

72

(* Monomorphic type variable *)

73

 Tunivar

74

(* Polymorphic type variable *)

75


76

type error =

77

 Unbound_value of ident

78

 Already_bound of ident

79

 Already_defined of ident

80

 Undefined_var of ISet.t

81

 Declared_but_undefined of ident

82

 Unbound_type of ident

83

 Not_a_dimension

84

 Not_a_constant

85

 Assigned_constant of ident

86

 WrongArity of int * int

87

 WrongMorphism of int * int

88

 Type_mismatch of ident

89

 Type_clash of t * t

90

 Poly_imported_node of ident

91


92

exception Unify of t * t

93


94

exception Error of Location.t * error

95


96

val is_real_type : t > bool

97


98

val is_int_type : t > bool

99


100

val is_bool_type : t > bool

101


102

val is_const_type : t > ident > bool

103


104

val is_static_type : t > bool

105


106

val is_array_type : t > bool

107


108

val is_dimension_type : t > bool

109


110

val is_address_type : t > bool

111


112

val is_generic_type : t > bool

113


114

val pp : Format.formatter > t > unit

115


116

val repr : t > t

117


118

val dynamic_type : t > t

119


120

val type_desc : t > type_desc

121


122

val new_var : unit > t

123


124

val new_univar : unit > t

125


126

val new_ty : type_desc > t

127


128

val type_int : type_desc

129


130

val type_real : type_desc

131


132

val type_bool : type_desc

133


134

val type_string : type_desc

135


136

val array_element_type : t > t

137


138

val type_list_of_type : t > t list

139


140

val pp_node_ty : Format.formatter > t > unit

141


142

val get_clock_base_type : t > t option

143


144

val get_static_value : t > Dimension.t option

145


146

val types_of_tuple_type : t > t list

147


148

val is_tuple_type : t > bool

149


150

val type_of_type_list : t list > t

151


152

val split_arrow : t > t * t

153


154

val unclock_type : t > t

155


156

val bottom : t

157


158

val map_tuple_type : (t > t) > t > t

159


160

val array_base_type : t > t

161


162

val array_type_dimension : t > Dimension.t

163


164

val pp_error : Format.formatter > error > unit

165


166

val struct_field_type : t > ident > t

167


168

val array_type_multi_dimension : t > Dimension.t list

169

end

170


171

module Basic : BASIC_TYPES = struct

172

type t = Tstring  Tint  Treal  Tbool  Trat

173

(* Actually unused for now. Only place where it can appear is in a clock

174

declaration *)

175


176

let type_string_builder = Tstring

177


178

let type_int_builder = Tint

179


180

let type_real_builder = Treal

181


182

let type_bool_builder = Tbool

183


184

open Format

185


186

let pp fmt t =

187

match t with

188

 Tint >

189

fprintf fmt "int"

190

 Treal >

191

fprintf fmt "real"

192

 Tstring >

193

fprintf fmt "string"

194

 Tbool >

195

fprintf fmt "bool"

196

 Trat >

197

fprintf fmt "rat"

198


199

let pp_c = pp

200


201

let is_scalar_type t =

202

match t with Tbool  Tint  Treal > true  _ > false

203


204

let is_numeric_type t = match t with Tint  Treal > true  _ > false

205


206

let is_int_type t = t = Tint

207


208

let is_real_type t = t = Treal

209


210

let is_bool_type t = t = Tbool

211


212

let is_dimension_type t = match t with Tint  Tbool > true  _ > false

213


214

let is_unifiable b1 b2 = b1 == b2

215


216

let unify _ _ = ()

217

end

218


219

module Make (BasicT : BASIC_TYPES) = struct

220

module BasicT = BasicT

221


222

type basic_type = BasicT.t

223


224

type t = { mutable tdesc : type_desc; tid : int }

225


226

and type_desc =

227

 Tconst of ident

228

(* type constant *)

229

 Tbasic of basic_type

230

 Tclock of t

231

(* A type expression explicitely tagged as carrying a clock *)

232

 Tarrow of t * t

233

 Ttuple of t list

234

 Tenum of ident list

235

 Tstruct of (ident * t) list

236

 Tarray of Dimension.t * t

237

 Tstatic of Dimension.t * t

238

(* a type carried by a dimension expression *)

239

 Tlink of t

240

(* During unification, make links instead of substitutions *)

241

 Tvar

242

(* Monomorphic type variable *)

243

 Tunivar

244

(* Polymorphic type variable *)

245


246

type error =

247

 Unbound_value of ident

248

 Already_bound of ident

249

 Already_defined of ident

250

 Undefined_var of ISet.t

251

 Declared_but_undefined of ident

252

 Unbound_type of ident

253

 Not_a_dimension

254

 Not_a_constant

255

 Assigned_constant of ident

256

 WrongArity of int * int

257

 WrongMorphism of int * int

258

 Type_mismatch of ident

259

 Type_clash of t * t

260

 Poly_imported_node of ident

261


262

exception Unify of t * t

263


264

exception Error of Location.t * error

265


266

let mk_basic t = Tbasic t

267


268

(* Prettyprint*)

269

open Format

270


271

let rec pp_struct_ty_field pp_basic fmt (label, ty) =

272

fprintf fmt "%a : %a" pp_print_string label (pp_ty_param pp_basic) ty

273


274

and pp_ty_param pp_basic fmt ty =

275

let pp_ty = pp_ty_param pp_basic in

276

match ty.tdesc with

277

 Tvar >

278

fprintf fmt "_%s" (name_of_type ty.tid)

279

 Tbasic t >

280

pp_basic fmt t

281

 Tclock t >

282

fprintf fmt "%a%s" pp_ty t (if !Options.kind2_print then "" else " clock")

283

 Tstatic (_, t) >

284

pp_ty fmt t

285

(* fprintf fmt "(%a:%a)" Dimension.pp_dimension d pp_ty t *)

286

 Tconst t >

287

fprintf fmt "%s" t

288

 Tarrow (ty1, ty2) >

289

fprintf fmt "%a > %a" pp_ty ty1 pp_ty ty2

290

 Ttuple tylist >

291

fprintf

292

fmt

293

"(%a)"

294

(pp_print_list ~pp_sep:(fun fmt () > pp_print_string fmt " * ") pp_ty)

295

tylist

296

 Tenum taglist >

297

fprintf fmt "enum {%a }" (pp_comma_list pp_print_string) taglist

298

 Tstruct fieldlist >

299

fprintf

300

fmt

301

"struct {%a }"

302

(pp_print_list ~pp_sep:pp_print_semicolon (pp_struct_ty_field pp_basic))

303

fieldlist

304

 Tarray (e, ty) >

305

fprintf fmt "%a^%a" pp_ty ty Dimension.pp e

306

 Tlink ty >

307

pp_ty fmt ty

308

 Tunivar >

309

fprintf fmt "'%s" (name_of_type ty.tid)

310


311

let pp = pp_ty_param BasicT.pp

312


313

let rec pp_node_struct_ty_field fmt (label, ty) =

314

fprintf fmt "%a : %a" pp_print_string label pp_node_ty ty

315


316

and pp_node_ty fmt ty =

317

match ty.tdesc with

318

 Tvar >

319

(*Format.eprintf "DEBUG:Types.pp_node@.";*)

320

fprintf fmt "_%s" (name_of_type ty.tid)

321

 Tbasic t >

322

BasicT.pp fmt t

323

 Tclock t >

324

fprintf

325

fmt

326

"%a%s"

327

pp_node_ty

328

t

329

(if !Options.kind2_print then "" else " clock")

330

 Tstatic (_, t) >

331

fprintf fmt "%a" pp_node_ty t

332

 Tconst t >

333

fprintf fmt "%s" t

334

 Tarrow (ty1, ty2) >

335

fprintf fmt "%a > %a" pp_node_ty ty1 pp_node_ty ty2

336

 Ttuple tylist >

337

fprintf

338

fmt

339

"(%a)"

340

(pp_print_list

341

~pp_sep:(fun fmt () > pp_print_string fmt "")

342

pp_node_ty)

343

tylist

344

 Tenum taglist >

345

fprintf fmt "enum {%a }" (pp_comma_list pp_print_string) taglist

346

 Tstruct fieldlist >

347

fprintf

348

fmt

349

"struct {%a }"

350

(pp_print_list ~pp_sep:pp_print_semicolon pp_node_struct_ty_field)

351

fieldlist

352

 Tarray (e, ty) >

353

fprintf fmt "%a^%a" pp_node_ty ty Dimension.pp e

354

 Tlink ty >

355

pp_node_ty fmt ty

356

 Tunivar >

357

fprintf fmt "'%s" (name_of_type ty.tid)

358


359

let pp_error fmt = function

360

 Unbound_value id >

361

fprintf fmt "Unknown value %s@." id

362

 Unbound_type id >

363

fprintf fmt "Unknown type %s@." id

364

 Already_bound id >

365

fprintf fmt "%s is already declared@." id

366

 Already_defined id >

367

fprintf fmt "Multiple definitions of variable %s@." id

368

 Not_a_constant >

369

fprintf fmt "This expression is not a constant@."

370

 Assigned_constant id >

371

fprintf fmt "The constant %s cannot be assigned@." id

372

 Not_a_dimension >

373

fprintf fmt "This expression is not a valid dimension@."

374

 WrongArity (ar1, ar2) >

375

fprintf fmt "Expecting %d argument(s), found %d@." ar1 ar2

376

 WrongMorphism (ar1, ar2) >

377

fprintf

378

fmt

379

"Expecting %d argument(s) for homomorphic extension, found %d@."

380

ar1

381

ar2

382

 Type_mismatch id >

383

fprintf fmt "Definition and declaration of type %s don't agree@." id

384

 Undefined_var vset >

385

fprintf

386

fmt

387

"No definition provided for variable(s): %a@."

388

(pp_comma_list pp_print_string)

389

(ISet.elements vset)

390

 Declared_but_undefined id >

391

fprintf fmt "%s is declared but not defined@." id

392

 Type_clash (ty1, ty2) >

393

Utils.reset_names ();

394

fprintf fmt "Expected type %a, got type %a@." pp ty1 pp ty2

395

 Poly_imported_node _ >

396

fprintf fmt "Imported nodes cannot have a polymorphic type@."

397


398

let new_id = ref (1)

399


400

let rec bottom : t = { tdesc = Tlink bottom; tid = 666 }

401


402

let new_ty desc =

403

incr new_id;

404

{ tdesc = desc; tid = !new_id }

405


406

let new_var () = new_ty Tvar

407


408

let new_univar () = new_ty Tunivar

409


410

let rec repr = function { tdesc = Tlink t'; _ } > repr t'  t > t

411


412

let get_static_value ty =

413

match (repr ty).tdesc with Tstatic (d, _) > Some d  _ > None

414


415

(* XXX: UNUSED *)

416

(* let get_field_type ty label =

417

* match (repr ty).tdesc with

418

*  Tstruct fl > (

419

* try Some (List.assoc label fl) with Not_found > None)

420

*  _ >

421

* None *)

422


423

let is_static_type ty =

424

match (repr ty).tdesc with Tstatic _ > true  _ > false

425


426

(* XXX: UNUSED *)

427

(* let rec is_scalar_type ty =

428

* match (repr ty).tdesc with

429

*  Tstatic (_, ty) >

430

* is_scalar_type ty

431

*  Tbasic t >

432

* BasicT.is_scalar_type t

433

*  _ >

434

* false *)

435


436

(* XXX: UNUSED *)

437

(* let rec is_numeric_type ty =

438

* match (repr ty).tdesc with

439

*  Tstatic (_, ty) >

440

* is_numeric_type ty

441

*  Tbasic t >

442

* BasicT.is_numeric_type t

443

*  _ >

444

* false *)

445


446

let rec is_real_type ty =

447

match (repr ty).tdesc with

448

 Tstatic (_, ty) >

449

is_real_type ty

450

 Tbasic t >

451

BasicT.is_real_type t

452

 _ >

453

false

454


455

let rec is_int_type ty =

456

match (repr ty).tdesc with

457

 Tstatic (_, ty) >

458

is_int_type ty

459

 Tbasic t >

460

BasicT.is_int_type t

461

 _ >

462

false

463


464

let rec is_bool_type ty =

465

match (repr ty).tdesc with

466

 Tstatic (_, ty) >

467

is_bool_type ty

468

 Tbasic t >

469

BasicT.is_bool_type t

470

 _ >

471

false

472


473

let rec is_const_type ty c =

474

match (repr ty).tdesc with

475

 Tstatic (_, ty) >

476

is_const_type ty c

477

 Tconst c' >

478

c = c'

479

 _ >

480

false

481


482

let get_clock_base_type ty =

483

match (repr ty).tdesc with Tclock ty > Some ty  _ > None

484


485

let unclock_type ty =

486

let ty = repr ty in

487

match ty.tdesc with Tclock ty' > ty'  _ > ty

488


489

let rec is_dimension_type ty =

490

match (repr ty).tdesc with

491

 Tbasic t >

492

BasicT.is_dimension_type t

493

 Tclock ty'  Tstatic (_, ty') >

494

is_dimension_type ty'

495

 _ >

496

false

497


498

let dynamic_type ty =

499

let ty = repr ty in

500

match ty.tdesc with Tstatic (_, ty') > ty'  _ > ty

501


502

let types_of_tuple_type ty =

503

match (repr ty).tdesc with Ttuple ts > ts  _ > []

504


505

let is_tuple_type ty =

506

match (repr ty).tdesc with Ttuple _ > true  _ > false

507


508

let map_tuple_type f ty =

509

let ty = dynamic_type ty in

510

match ty.tdesc with

511

 Ttuple ty_list >

512

{ ty with tdesc = Ttuple (List.map f ty_list) }

513

 _ >

514

f ty

515


516

let rec is_struct_type ty =

517

match (repr ty).tdesc with

518

 Tstruct _ >

519

true

520

 Tstatic (_, ty') >

521

is_struct_type ty'

522

 _ >

523

false

524


525

let struct_field_type ty field =

526

match (dynamic_type ty).tdesc with

527

 Tstruct fields > (

528

try List.assoc field fields with Not_found > assert false)

529

 _ >

530

assert false

531


532

let rec is_array_type ty =

533

match (repr ty).tdesc with

534

 Tarray _ >

535

true

536

 Tstatic (_, ty') >

537

is_array_type ty' (* looks strange !? *)

538

 _ >

539

false

540


541

let array_type_dimension ty =

542

match (dynamic_type ty).tdesc with

543

 Tarray (d, _) >

544

d

545

 _ >

546

eprintf "internal error: Types.array_type_dimension %a@." pp ty;

547

assert false

548


549

let rec array_type_multi_dimension ty =

550

match (dynamic_type ty).tdesc with

551

 Tarray (d, ty') >

552

d :: array_type_multi_dimension ty'

553

 _ >

554

[]

555


556

let array_element_type ty =

557

match (dynamic_type ty).tdesc with

558

 Tarray (_, ty') >

559

ty'

560

 _ >

561

eprintf "internal error: Types.array_element_type %a@." pp ty;

562

assert false

563


564

let rec array_base_type ty =

565

let ty = repr ty in

566

match ty.tdesc with

567

 Tarray (_, ty')  Tstatic (_, ty') >

568

array_base_type ty'

569

 _ >

570

ty

571


572

let is_address_type ty =

573

is_array_type ty  is_struct_type ty  (is_real_type ty && !Options.mpfr)

574


575

let rec is_generic_type ty =

576

match (dynamic_type ty).tdesc with

577

 Tarray (d, ty') >

578

(not (Dimension.is_const d))  is_generic_type ty'

579

 _ >

580

false

581


582

(** Splits [ty] into the [lhs,rhs] of an arrow type. Expects an arrow type

583

(ensured by language syntax) *)

584

let rec split_arrow ty =

585

match (repr ty).tdesc with

586

 Tarrow (tin, tout) >

587

tin, tout

588

 Tstatic (_, ty') >

589

split_arrow ty'

590

(* Functions are not first order, I don't think the var case needs to be

591

considered here *)

592

 _ >

593

eprintf "type %a is not a map@.Unable to split@.@?" pp ty;

594

assert false

595


596

(** Returns the type corresponding to a type list. *)

597

let type_of_type_list = function [ t ] > t  tyl > new_ty (Ttuple tyl)

598


599

let rec type_list_of_type ty =

600

match (repr ty).tdesc with

601

 Tstatic (_, ty) >

602

type_list_of_type ty

603

 Ttuple tl >

604

tl

605

 _ >

606

[ ty ]

607


608

(* XXX: UNUSED *)

609

(** [is_polymorphic ty] returns true if [ty] is polymorphic. *)

610

(* let rec is_polymorphic ty =

611

* match ty.tdesc with

612

*  Tenum _  Tvar  Tbasic _  Tconst _ >

613

* false

614

*  Tclock ty >

615

* is_polymorphic ty

616

*  Tarrow (ty1, ty2) >

617

* is_polymorphic ty1  is_polymorphic ty2

618

*  Ttuple tl >

619

* List.exists (fun t > is_polymorphic t) tl

620

*  Tstruct fl >

621

* List.exists (fun (_, t) > is_polymorphic t) fl

622

*  Tlink t' >

623

* is_polymorphic t'

624

*  Tarray (d, ty)  Tstatic (d, ty) >

625

* Dimension.is_polymorphic d  is_polymorphic ty

626

*  Tunivar >

627

* true *)

628


629

(* XXX: UNUSED *)

630

(* let mktyptuple nb typ =

631

* let array = Array.make nb typ in

632

* Ttuple (Array.to_list array) *)

633


634

let type_desc t = t.tdesc

635


636

let type_int = mk_basic BasicT.type_int_builder

637


638

let type_real = mk_basic BasicT.type_real_builder

639


640

let type_bool = mk_basic BasicT.type_bool_builder

641


642

let type_string = mk_basic BasicT.type_string_builder

643

end

644


645

include Make (Basic)

646


647

(* Local Variables: *)

648

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

649

(* End: *)
