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

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

15

open Utils

16

open Dimension

17


18

module type BASIC_TYPES =

19

sig

20

type t

21

val pp: Format.formatter > t > unit

22

val pp_c: Format.formatter > t > unit

23

val is_scalar_type: t > bool

24

val is_numeric_type: t > bool

25

val is_int_type: t > bool

26

val is_real_type: t > bool

27

val is_bool_type: t > bool

28

val is_dimension_type: t > bool

29

val type_int_builder: t

30

val type_real_builder: t

31

val type_bool_builder: t

32

val type_string_builder: t

33

val unify: t > t > unit

34

val is_unifiable: t > t > bool

35

end

36


37

module Basic =

38

struct

39

type t =

40

 Tstring

41

 Tint

42

 Treal

43

 Tbool

44

 Trat (* Actually unused for now. Only place where it can appear is

45

in a clock declaration *)

46


47

let type_string_builder = Tstring

48

let type_int_builder = Tint

49

let type_real_builder = Treal

50

let type_bool_builder = Tbool

51


52

open Format

53

let pp fmt t =

54

match t with

55

 Tint >

56

fprintf fmt "int"

57

 Treal >

58

fprintf fmt "real"

59

 Tstring >

60

fprintf fmt "string"

61

 Tbool >

62

fprintf fmt "bool"

63

 Trat >

64

fprintf fmt "rat"

65


66

let pp_c = pp

67


68

let is_scalar_type t =

69

match t with

70

 Tbool

71

 Tint

72

 Treal > true

73

 _ > false

74


75


76

let is_numeric_type t =

77

match t with

78

 Tint

79

 Treal > true

80

 _ > false

81


82

let is_int_type t = t = Tint

83

let is_real_type t = t = Treal

84

let is_bool_type t = t = Tbool

85


86

let is_dimension_type t =

87

match t with

88

 Tint

89

 Tbool > true

90

 _ > false

91


92

let is_unifiable b1 b2 = b1 == b2

93

let unify _ _ = ()

94

end

95


96


97


98

module Make(BasicT : BASIC_TYPES) =

99

struct

100


101

module BasicT = BasicT

102

type basic_type = BasicT.t

103

type type_expr =

104

{mutable tdesc: type_desc;

105

tid: int}

106

and type_desc =

107

 Tconst of ident (* type constant *)

108

 Tbasic of basic_type

109

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

110

 Tarrow of type_expr * type_expr

111

 Ttuple of type_expr list

112

 Tenum of ident list

113

 Tstruct of (ident * type_expr) list

114

 Tarray of dim_expr * type_expr

115

 Tstatic of dim_expr * type_expr (* a type carried by a dimension expression *)

116

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

117

 Tvar (* Monomorphic type variable *)

118

 Tunivar (* Polymorphic type variable *)

119


120

(* {mutable tdesc: type_desc; *)

121

(* tid: int} *)

122


123

(* and type_desc = *)

124

(*  Tconst of ident (\* type constant *\) *)

125

(*  Tbasic of BasicT.t *)

126

(*  Tclock of type_expr (\* A type expression explicitely tagged as carrying a clock *\) *)

127

(*  Tarrow of type_expr * type_expr *)

128

(*  Ttuple of type_expr list *)

129

(*  Tenum of ident list *)

130

(*  Tstruct of (ident * type_expr) list *)

131

(*  Tarray of dim_expr * type_expr *)

132

(*  Tstatic of dim_expr * type_expr (\* a type carried by a dimension expression *\) *)

133

(*  Tlink of type_expr (\* During unification, make links instead of substitutions *\) *)

134

(*  Tvar (\* Monomorphic type variable *\) *)

135

(*  Tunivar (\* Polymorphic type variable *\) *)

136


137

type error =

138

Unbound_value of ident

139

 Already_bound of ident

140

 Already_defined of ident

141

 Undefined_var of ISet.t

142

 Declared_but_undefined of ident

143

 Unbound_type of ident

144

 Not_a_dimension

145

 Not_a_constant

146

 Assigned_constant of ident

147

 WrongArity of int * int

148

 WrongMorphism of int * int

149

 Type_mismatch of ident

150

 Type_clash of type_expr * type_expr

151

 Poly_imported_node of ident

152


153

exception Unify of type_expr * type_expr

154

exception Error of Location.t * error

155


156

let mk_basic t = Tbasic t

157


158


159

(* Prettyprint*)

160

open Format

161


162

let rec print_struct_ty_field pp_basic fmt (label, ty) =

163

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

164

and print_ty_param pp_basic fmt ty =

165

let print_ty = print_ty_param pp_basic in

166

match ty.tdesc with

167

 Tvar >

168

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

169

 Tbasic t > pp_basic fmt t

170

 Tclock t >

171

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

172

 Tstatic (d, t) > print_ty fmt t

173

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

174

 Tconst t >

175

fprintf fmt "%s" t

176

 Tarrow (ty1,ty2) >

177

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

178

 Ttuple tylist >

179

fprintf fmt "(%a)"

180

(Utils.fprintf_list ~sep:" * " print_ty) tylist

181

 Tenum taglist >

182

fprintf fmt "enum {%a }"

183

(Utils.fprintf_list ~sep:", " pp_print_string) taglist

184

 Tstruct fieldlist >

185

fprintf fmt "struct {%a }"

186

(Utils.fprintf_list ~sep:"; " (print_struct_ty_field pp_basic)) fieldlist

187

 Tarray (e, ty) >

188

fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e

189

 Tlink ty >

190

print_ty fmt ty

191

 Tunivar >

192

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

193


194

let print_ty = print_ty_param BasicT.pp

195


196


197

let rec print_node_struct_ty_field fmt (label, ty) =

198

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

199

and print_node_ty fmt ty =

200

match ty.tdesc with

201

 Tvar > begin

202

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

203

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

204

end

205

 Tbasic t > BasicT.pp fmt t

206

 Tclock t >

207

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

208

 Tstatic (_, t) >

209

fprintf fmt "%a" print_node_ty t

210

 Tconst t >

211

fprintf fmt "%s" t

212

 Tarrow (ty1,ty2) >

213

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

214

 Ttuple tylist >

215

fprintf fmt "(%a)"

216

(Utils.fprintf_list ~sep:"*" print_node_ty) tylist

217

 Tenum taglist >

218

fprintf fmt "enum {%a }"

219

(Utils.fprintf_list ~sep:", " pp_print_string) taglist

220

 Tstruct fieldlist >

221

fprintf fmt "struct {%a }"

222

(Utils.fprintf_list ~sep:"; " print_node_struct_ty_field) fieldlist

223

 Tarray (e, ty) >

224

fprintf fmt "%a^%a" print_node_ty ty Dimension.pp_dimension e

225

 Tlink ty >

226

print_node_ty fmt ty

227

 Tunivar >

228

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

229


230

let pp_error fmt = function

231

 Unbound_value id >

232

fprintf fmt "Unknown value %s@." id

233

 Unbound_type id >

234

fprintf fmt "Unknown type %s@." id

235

 Already_bound id >

236

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

237

 Already_defined id >

238

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

239

 Not_a_constant >

240

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

241

 Assigned_constant id >

242

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

243

 Not_a_dimension >

244

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

245

 WrongArity (ar1, ar2) >

246

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

247

 WrongMorphism (ar1, ar2) >

248

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

249

 Type_mismatch id >

250

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

251

 Undefined_var vset >

252

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

253

(Utils.fprintf_list ~sep:"," pp_print_string)

254

(ISet.elements vset)

255

 Declared_but_undefined id >

256

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

257

 Type_clash (ty1,ty2) >

258

Utils.reset_names ();

259

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

260

 Poly_imported_node id >

261

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

262


263


264

let new_id = ref (1)

265


266

let rec bottom =

267

{ tdesc = Tlink bottom; tid = 666 }

268


269

let new_ty desc =

270

incr new_id; {tdesc = desc; tid = !new_id }

271


272

let new_var () =

273

new_ty Tvar

274


275

let new_univar () =

276

new_ty Tunivar

277


278

let rec repr =

279

function

280

{tdesc = Tlink t'} >

281

repr t'

282

 t > t

283


284

let get_static_value ty =

285

match (repr ty).tdesc with

286

 Tstatic (d, _) > Some d

287

 _ > None

288


289

let get_field_type ty label =

290

match (repr ty).tdesc with

291

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

292

 _ > None

293


294

let rec is_static_type ty =

295

match (repr ty).tdesc with

296

 Tstatic (_, ty) > true

297

 _ > false

298


299

let rec is_scalar_type ty =

300

match (repr ty).tdesc with

301

 Tstatic (_, ty) > is_scalar_type ty

302

 Tbasic t > BasicT.is_scalar_type t

303

 _ > false

304


305

let rec is_numeric_type ty =

306

match (repr ty).tdesc with

307

 Tstatic (_, ty) > is_numeric_type ty

308

 Tbasic t > BasicT.is_numeric_type t

309

 _ > false

310


311

let rec is_real_type ty =

312

match (repr ty).tdesc with

313

 Tstatic (_, ty) > is_real_type ty

314

 Tbasic t > BasicT.is_real_type t

315

 _ > false

316


317

let rec is_int_type ty =

318

match (repr ty).tdesc with

319

 Tstatic (_, ty) > is_int_type ty

320

 Tbasic t > BasicT.is_int_type t

321

 _ > false

322


323

let rec is_bool_type ty =

324

match (repr ty).tdesc with

325

 Tstatic (_, ty) > is_bool_type ty

326

 Tbasic t > BasicT.is_bool_type t

327

 _ > false

328


329

let rec is_const_type ty c =

330

match (repr ty).tdesc with

331

 Tstatic (_, ty) > is_const_type ty c

332

 Tconst c' > c = c'

333

 _ > false

334


335

let get_clock_base_type ty =

336

match (repr ty).tdesc with

337

 Tclock ty > Some ty

338

 _ > None

339


340

let unclock_type ty =

341

let ty = repr ty in

342

match ty.tdesc with

343

 Tclock ty' > ty'

344

 _ > ty

345


346

let rec is_dimension_type ty =

347

match (repr ty).tdesc with

348

 Tbasic t > BasicT.is_dimension_type t

349

 Tclock ty'

350

 Tstatic (_, ty') > is_dimension_type ty'

351

 _ > false

352


353

let dynamic_type ty =

354

let ty = repr ty in

355

match ty.tdesc with

356

 Tstatic (_, ty') > ty'

357

 _ > ty

358


359

let is_tuple_type ty =

360

match (repr ty).tdesc with

361

 Ttuple _ > true

362

 _ > false

363


364

let map_tuple_type f ty =

365

let ty = dynamic_type ty in

366

match ty.tdesc with

367

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

368

 _ > f ty

369


370

let rec is_struct_type ty =

371

match (repr ty).tdesc with

372

 Tstruct _ > true

373

 Tstatic (_, ty') > is_struct_type ty'

374

 _ > false

375


376

let struct_field_type ty field =

377

match (dynamic_type ty).tdesc with

378

 Tstruct fields >

379

(try

380

List.assoc field fields

381

with Not_found > assert false)

382

 _ > assert false

383


384

let rec is_array_type ty =

385

match (repr ty).tdesc with

386

 Tarray _ > true

387

 Tstatic (_, ty') > is_array_type ty' (* looks strange !? *)

388

 _ > false

389


390

let array_type_dimension ty =

391

match (dynamic_type ty).tdesc with

392

 Tarray (d, _) > d

393

 _ > (Format.eprintf "internal error: Types.array_type_dimension %a@." print_ty ty; assert false)

394


395

let rec array_type_multi_dimension ty =

396

match (dynamic_type ty).tdesc with

397

 Tarray (d, ty') > d :: array_type_multi_dimension ty'

398

 _ > []

399


400

let array_element_type ty =

401

match (dynamic_type ty).tdesc with

402

 Tarray (_, ty') > ty'

403

 _ > (Format.eprintf "internal error: Types.array_element_type %a@." print_ty ty; assert false)

404


405

let rec array_base_type ty =

406

let ty = repr ty in

407

match ty.tdesc with

408

 Tarray (_, ty')

409

 Tstatic (_, ty') > array_base_type ty'

410

 _ > ty

411


412

let is_address_type ty =

413

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

414


415

let rec is_generic_type ty =

416

match (dynamic_type ty).tdesc with

417

 Tarray (d, ty') >

418

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

419

 _ > false

420


421

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

422

(ensured by language syntax) *)

423

let rec split_arrow ty =

424

match (repr ty).tdesc with

425

 Tarrow (tin,tout) > tin,tout

426

 Tstatic (_, ty') > split_arrow ty'

427

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

428

needs to be considered here *)

429

 _ > Format.eprintf "type %a is not a map@.Unable to split@.@?" print_ty ty; assert false

430


431

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

432

let type_of_type_list tyl =

433

if (List.length tyl) > 1 then

434

new_ty (Ttuple tyl)

435

else

436

List.hd tyl

437


438

let rec type_list_of_type ty =

439

match (repr ty).tdesc with

440

 Tstatic (_, ty) > type_list_of_type ty

441

 Ttuple tl > tl

442

 _ > [ty]

443


444

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

445

let rec is_polymorphic ty =

446

match ty.tdesc with

447

 Tenum _  Tvar  Tbasic _  Tconst _ > false

448

 Tclock ty > is_polymorphic ty

449

 Tarrow (ty1,ty2) > (is_polymorphic ty1)  (is_polymorphic ty2)

450

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

451

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

452

 Tlink t' > is_polymorphic t'

453

 Tarray (d, ty)

454

 Tstatic (d, ty) > Dimension.is_polymorphic d  is_polymorphic ty

455

 Tunivar > true

456


457


458

let mktyptuple nb typ =

459

let array = Array.make nb typ in

460

Ttuple (Array.to_list array)

461


462

let type_desc t = t.tdesc

463


464


465


466

let type_int = mk_basic BasicT.type_int_builder

467

let type_real = mk_basic BasicT.type_real_builder

468

let type_bool = mk_basic BasicT.type_bool_builder

469

let type_string = mk_basic BasicT.type_string_builder

470


471

end

472


473


474

module type S =

475

sig

476

module BasicT: BASIC_TYPES

477

type basic_type = BasicT.t

478

type type_expr =

479

{mutable tdesc: type_desc;

480

tid: int}

481

and type_desc =

482

 Tconst of ident (* type constant *)

483

 Tbasic of basic_type

484

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

485

 Tarrow of type_expr * type_expr

486

 Ttuple of type_expr list

487

 Tenum of ident list

488

 Tstruct of (ident * type_expr) list

489

 Tarray of dim_expr * type_expr

490

 Tstatic of dim_expr * type_expr (* a type carried by a dimension expression *)

491

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

492

 Tvar (* Monomorphic type variable *)

493

 Tunivar (* Polymorphic type variable *)

494


495

type error =

496

Unbound_value of ident

497

 Already_bound of ident

498

 Already_defined of ident

499

 Undefined_var of ISet.t

500

 Declared_but_undefined of ident

501

 Unbound_type of ident

502

 Not_a_dimension

503

 Not_a_constant

504

 Assigned_constant of ident

505

 WrongArity of int * int

506

 WrongMorphism of int * int

507

 Type_mismatch of ident

508

 Type_clash of type_expr * type_expr

509

 Poly_imported_node of ident

510


511

exception Unify of type_expr * type_expr

512

exception Error of Location.t * error

513


514

val is_real_type: type_expr > bool

515

val is_int_type: type_expr > bool

516

val is_bool_type: type_expr > bool

517

val is_const_type: type_expr > ident > bool

518

val is_static_type: type_expr > bool

519

val is_array_type: type_expr > bool

520

val is_dimension_type: type_expr > bool

521

val is_address_type: type_expr > bool

522

val is_generic_type: type_expr > bool

523

val print_ty: Format.formatter > type_expr > unit

524

val repr: type_expr > type_expr

525

val dynamic_type: type_expr > type_expr

526

val type_desc: type_expr > type_desc

527

val new_var: unit > type_expr

528

val new_univar: unit > type_expr

529

val new_ty: type_desc > type_expr

530

val type_int: type_desc

531

val type_real: type_desc

532

val type_bool: type_desc

533

val type_string: type_desc

534

val array_element_type: type_expr > type_expr

535

val type_list_of_type: type_expr > type_expr list

536

val print_node_ty: Format.formatter > type_expr > unit

537

val get_clock_base_type: type_expr > type_expr option

538

val get_static_value: type_expr > Dimension.dim_expr option

539

val is_tuple_type: type_expr > bool

540

val type_of_type_list: type_expr list > type_expr

541

val split_arrow: type_expr > type_expr * type_expr

542

val unclock_type: type_expr > type_expr

543

val bottom: type_expr

544

val map_tuple_type: (type_expr > type_expr) > type_expr > type_expr

545

val array_base_type: type_expr > type_expr

546

val array_type_dimension: type_expr > Dimension.dim_expr

547

val pp_error: Format.formatter > error > unit

548

val struct_field_type: type_expr > ident > type_expr

549

val array_type_multi_dimension: type_expr > Dimension.dim_expr list

550

end (* with type type_expr = BasicT.t type_expr_gen *)

551


552

module type Sbasic = S with type BasicT.t = Basic.t

553


554

module Main : Sbasic = Make (Basic)

555

include Main

556


557


558

(* Local Variables: *)

559

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

560

(* End: *)
