1

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

2

(* *)

3

(* The LustreC compiler toolset / The LustreC Development Team *)

4

(* Copyright 2012   ONERA  CNRS  INPT  LIFL *)

5

(* *)

6

(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)

7

(* under the terms of the GNU Lesser General Public License *)

8

(* version 2.1. *)

9

(* *)

10

(* This file was originally from the Prelude compiler *)

11

(* *)

12

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

13


14

(** Main typing module. Classic inference algorithm with destructive

15

unification. *)

16


17

let debug fmt args = () (* Format.eprintf "%a" *)

18

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

19

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

20

identifier redefinition allowed. *)

21


22

open Utils

23

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

24

overwritten, yet this makes notations far lighter.*)

25

open Lustre_types

26

open Corelang

27

open Format

28


29


30

(* TODO general remark: expect in the add_vdelc, it seems to me that

31

all the pairs (env, vd_env) should be replace with just env, since

32

vd_env is never used and the env element is always extract with a

33

fst *)

34


35


36

module type EXPR_TYPE_HUB =

37

sig

38

type type_expr

39

val import: Types.Main.type_expr > type_expr

40

val export: type_expr > Types.Main.type_expr

41

end

42


43

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

44

struct

45


46

module TP = Type_predef.Make (T)

47

include TP

48


49

let pp_typing_env fmt env =

50

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]

57

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

58

let rec occurs tvar ty =

59

let ty = repr ty in

60

match type_desc ty with

61

 Tvar > ty=tvar

62

 Tarrow (t1, t2) >

63

(occurs tvar t1)  (occurs tvar t2)

64

 Ttuple tl >

65

List.exists (occurs tvar) tl

66

 Tstruct fl >

67

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

68

 Tarray (_, t)

69

 Tstatic (_, t)

70

 Tclock t

71

 Tlink t > occurs tvar t

72

 Tenum _  Tconst _  Tunivar  Tbasic _ > false

73


74

(** Promote monomorphic type variables to polymorphic type

75

variables. *)

76

(* Generalize by sideeffects *)

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; generalize t2

84

 Ttuple tl >

85

List.iter generalize tl

86

 Tstruct fl >

87

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

88

 Tstatic (d, t)

89

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

90

 Tclock t

91

 Tlink t >

92

generalize t

93

 Tenum _  Tconst _  Tunivar  Tbasic _ > ()

94


95

(** Downgrade polymorphic type variables to monomorphic type

96

variables *)

97

let rec instantiate inst_vars inst_dim_vars ty =

98

let ty = repr ty in

99

match ty.tdesc with

100

 Tenum _  Tconst _  Tvar  Tbasic _ > ty

101

 Tarrow (t1,t2) >

102

{ty with tdesc =

103

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

104

 Ttuple tlist >

105

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

106

 Tstruct flist >

107

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

108

 Tclock t >

109

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

110

 Tstatic (d, t) >

111

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

112

 Tarray (d, t) >

113

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

114

 Tlink t >

115

(* should not happen *)

116

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

117

 Tunivar >

118

try

119

List.assoc ty.tid !inst_vars

120

with Not_found >

121

let var = new_var () in

122

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

123

var

124


125


126


127

let basic_coretype_type t =

128

if is_real_type t then Tydec_real else

129

if is_int_type t then Tydec_int else

130

if is_bool_type t then Tydec_bool else

131

assert false

132


133

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

134

let rec type_coretype type_dim cty =

135

match (*get_repr_type*) cty with

136

 Tydec_any > new_var ()

137

 Tydec_int > type_int

138

 Tydec_real > (* Type_predef. *)type_real

139

(*  Tydec_float > Type_predef.type_real *)

140

 Tydec_bool > (* Type_predef. *)type_bool

141

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

142

 Tydec_const c > (* Type_predef. *)type_const c

143

 Tydec_enum tl > (* Type_predef. *)type_enum tl

144

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

145

 Tydec_array (d, ty) >

146

begin

147

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

148

type_dim d;

149

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

150

end

151


152

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

153

let rec coretype_type ty =

154

match (repr ty).tdesc with

155

 Tvar > Tydec_any

156

 Tbasic _ > basic_coretype_type ty

157

 Tconst c > Tydec_const c

158

 Tclock t > Tydec_clock (coretype_type t)

159

 Tenum tl > Tydec_enum tl

160

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

161

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

162

 Tstatic (_, t) > coretype_type t

163

 _ > assert false

164


165

let get_coretype_definition tname =

166

try

167

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

168

match top.top_decl_desc with

169

 TypeDef tdef > tdef.tydef_desc

170

 _ > assert false

171

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

172


173

let get_type_definition tname =

174

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

175


176

(* Equality on ground types only *)

177

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

178

let rec eq_ground t1 t2 =

179

let t1 = repr t1 in

180

let t2 = repr t2 in

181

t1==t2 

182

match t1.tdesc, t2.tdesc with

183

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

184

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

185

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

186

 Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' > List.for_all2 (fun (_, t) (_, t') > eq_ground t t') fl fl'

187

 (Tconst t, _) >

188

let def_t = get_type_definition t in

189

eq_ground def_t t2

190

 (_, Tconst t) >

191

let def_t = get_type_definition t in

192

eq_ground t1 def_t

193

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

194

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

195

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

196

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

197

 _ > false

198


199

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

200

using standard destructive unification.

201

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

202

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

203

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

204

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

205

If [semi] unification is required,

206

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

207

and constants are handled differently.*)

208

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

209

let rec unif t1 t2 =

210

let t1 = repr t1 in

211

let t2 = repr t2 in

212

if t1==t2 then

213

()

214

else

215

match t1.tdesc,t2.tdesc with

216

(* strictly subtyping cases first *)

217

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

218

unif t1 t2

219

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

220

unif t1 t2

221

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

222

 Tvar, Tvar >

223

if t1.tid < t2.tid then

224

t2.tdesc < Tlink t1

225

else

226

t1.tdesc < Tlink t2

227

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

228

t1.tdesc < Tlink t2

229

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

230

t2.tdesc < Tlink t1

231

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

232

begin

233

unif t2 t2';

234

unif t1' t1

235

end

236

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

237

List.iter2 unif tl tl'

238

 Ttuple [t1] , _ > unif t1 t2

239

 _ , Ttuple [t2] > unif t1 t2

240

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

241

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

242

 Tclock _, Tstatic _

243

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

244

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

245

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

246

 Tunivar, _  _, Tunivar > ()

247

 (Tconst t, _) >

248

let def_t = get_type_definition t in

249

unif def_t t2

250

 (_, Tconst t) >

251

let def_t = get_type_definition t in

252

unif t1 def_t

253

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

254

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

255

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

256

let eval_const =

257

if semi

258

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

259

else (fun c > None) in

260

begin

261

unif t1' t2';

262

Dimension.eval Basic_library.eval_env eval_const e1;

263

Dimension.eval Basic_library.eval_env eval_const e2;

264

Dimension.unify ~semi:semi e1 e2;

265

end

266

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

267

for numerical constants with non static ones for variables with

268

possible machine types *)

269

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

270

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

271

in unif t1 t2

272


273

(* Expected type ty1, got type ty2 *)

274

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

275

try

276

unify ~sub:sub ~semi:semi ty1 ty2

277

with

278

 Unify _ >

279

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

280

 Dimension.Unify _ >

281

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

282


283


284

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

285

(* Typing function for each basic AST construct *)

286

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

287


288

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

289

if Hashtbl.mem field_table label

290

then let tydef = Hashtbl.find field_table label in

291

let tydec = (typedef_of_top tydef).tydef_desc in

292

let tydec_struct = get_struct_type_fields tydec in

293

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

294

begin

295

try_unify ty_label (type_const ~is_annot loc c) loc;

296

type_coretype (fun d > ()) tydec

297

end

298

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

299


300

and type_const ?(is_annot=false) loc c =

301

match c with

302

 Const_int _ > (* Type_predef. *)type_int

303

 Const_real _ > (* Type_predef. *)type_real

304

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

305

let ty = new_var () in

306

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

307

(* Type_predef. *)type_array d ty

308

 Const_tag t >

309

if Hashtbl.mem tag_table t

310

then

311

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

312

let tydec =

313

if is_user_type tydef.tydef_desc

314

then Tydec_const tydef.tydef_id

315

else tydef.tydef_desc in

316

type_coretype (fun d > ()) tydec

317

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

318

 Const_struct fl >

319

let ty_struct = new_var () in

320

begin

321

let used =

322

List.fold_left

323

(fun acc (l, c) >

324

if List.mem l acc

325

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

326

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

327

[] fl in

328

try

329

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

330

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

331

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

332

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

333

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

334

with Not_found >

335

ty_struct

336

end

337

 Const_string _  Const_modeid _ >

338

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

339


340

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

341

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

342

[env] is a pair composed of:

343

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

344

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

345

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

346

propagation policy in Lustre.

347

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

348

later discovered to be clocks during the typing process.

349

*)

350

let check_constant loc const_expected const_real =

351

if const_expected && not const_real

352

then raise (Error (loc, Not_a_constant))

353


354

let rec type_add_const env const arg targ =

355

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

356

if const

357

then let d =

358

if is_dimension_type targ

359

then dimension_of_expr arg

360

else Dimension.mkdim_var () in

361

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

362

Dimension.eval Basic_library.eval_env eval_const d;

363

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

364

(match (* Types. *)get_static_value targ with

365

 None > ()

366

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

367

real_static_type

368

else targ

369


370

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

371

used during node applications and assignments *)

372

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

373

let loc = real_arg.expr_loc in

374

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

375

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

376

(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)

377

try_unify ~sub:sub formal_type real_type loc

378


379

(* typing an application implies:

380

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

381

 checking type adequation between formal and real arguments

382

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

383

it in many calls

384

*)

385

and type_appl env in_main loc const f args =

386

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

387

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

388

then

389

try

390

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

391

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

392

with

393

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

394


395

else (

396

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

397

)

398


399

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

400

and type_dependent_call env in_main loc const f targs =

401

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

402

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

403

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

404

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

405

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

406

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

407

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

408

let tins = type_list_of_type tins in

409

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

410

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

411

else

412

begin

413

List.iter2 (

414

fun (a,t) ti >

415

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

416

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

417

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

418

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

419


420

)

421

targs

422

tins;

423

touts

424

end

425


426

(* type a simple call without dependent types

427

but possible homomorphic extension.

428

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

429

and type_simple_call env in_main loc const f targs =

430

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

431

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

432

type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;

433

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

434

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

435

touts

436


437

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

438

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

439

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

440

let resulting_ty =

441

match expr.expr_desc with

442

 Expr_const c >

443

let ty = type_const ~is_annot expr.expr_loc c in

444

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

445

expr.expr_type < Expr_type_hub.export ty;

446

ty

447

 Expr_ident v >

448

let tyv =

449

try

450

Env.lookup_value (fst env) v

451

with Not_found >

452

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

453

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

454

in

455

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

456

let ty' =

457

if const

458

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

459

else new_var () in

460

try_unify ty ty' expr.expr_loc;

461

expr.expr_type < Expr_type_hub.export ty;

462

ty

463

 Expr_array elist >

464

let ty_elt = new_var () in

465

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

466

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

467

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

468

expr.expr_type < Expr_type_hub.export ty;

469

ty

470

 Expr_access (e1, d) >

471

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

472

let ty_elt = new_var () in

473

let d = Dimension.mkdim_var () in

474

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

475

expr.expr_type < Expr_type_hub.export ty_elt;

476

ty_elt

477

 Expr_power (e1, d) >

478

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

479

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

480

Dimension.eval Basic_library.eval_env eval_const d;

481

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

482

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

483

expr.expr_type < Expr_type_hub.export ty;

484

ty

485

 Expr_tuple elist >

486

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

487

expr.expr_type < Expr_type_hub.export ty;

488

ty

489

 Expr_ite (c, t, e) >

490

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

491

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

492

expr.expr_type < Expr_type_hub.export ty;

493

ty

494

 Expr_appl (id, args, r) >

495

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

496

expression *)

497

(match r with

498

 None > ()

499

 Some c >

500

check_constant expr.expr_loc const false;

501

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

502

let args_list = expr_list_of_expr args in

503

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

504

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

505

args.expr_type < Expr_type_hub.export targs;

506

expr.expr_type < Expr_type_hub.export touts;

507

touts

508

 Expr_fby (e1,e2)

509

 Expr_arrow (e1,e2) >

510

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

511

check_constant expr.expr_loc const false;

512

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

513

expr.expr_type < Expr_type_hub.export ty;

514

ty

515

 Expr_pre e >

516

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

517

check_constant expr.expr_loc const false;

518

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

519

expr.expr_type < Expr_type_hub.export ty;

520

ty

521

 Expr_when (e1,c,l) >

522

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

523

check_constant expr.expr_loc const false;

524

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

525

let expr_c = expr_of_ident c expr.expr_loc in

526

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

527

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

528

expr.expr_type < Expr_type_hub.export ty;

529

ty

530

 Expr_merge (c,hl) >

531

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

532

check_constant expr.expr_loc const false;

533

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

534

let expr_c = expr_of_ident c expr.expr_loc in

535

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

536

type_subtyping_arg env in_main ~sub:false const expr_c typ_l;

537

expr.expr_type < Expr_type_hub.export typ_out;

538

typ_out

539

in

540

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

541

resulting_ty

542


543

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

544

let typ_in = new_var () in

545

let typ_out = new_var () in

546

try

547

let used_labels =

548

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

549

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

550

type_subtyping_arg env in_main const h typ_out;

551

if List.mem t accu

552

then raise (Error (loc, Already_bound t))

553

else t :: accu) [] hl in

554

let type_labels = get_enum_type_tags (coretype_type typ_in) in

555

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

556

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

557

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

558

else (typ_in, typ_out)

559

with Unify (t1, t2) >

560

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

561


562

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

563

let type_eexpr env eexpr =

564

(type_expr

565

~is_annot:true

566

env

567

false (* not in main *)

568

false (* not a const *)

569

eexpr.eexpr_qfexpr)

570


571


572

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

573

let type_eq env in_main undefined_vars eq =

574

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

575

(* Check undefined variables, type lhs *)

576

let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v > expr_of_ident v eq.eq_loc) eq.eq_lhs) in

577

let ty_lhs = type_expr env in_main false expr_lhs in

578

(* Check multiple variable definitions *)

579

let define_var id uvars =

580

if ISet.mem id uvars

581

then ISet.remove id uvars

582

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

583

in

584

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

585

let ty_lhs =

586

type_of_type_list

587

(List.map2 (fun ty id >

588

if get_static_value ty <> None

589

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

590

match get_clock_base_type ty with

591

 None > ty

592

 Some ty > ty)

593

(type_list_of_type ty_lhs) eq.eq_lhs) in

594

let undefined_vars =

595

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

596

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

597

to a (always nonconstant) lhs variable *)

598

type_subtyping_arg env in_main false eq.eq_rhs ty_lhs;

599

undefined_vars

600


601


602

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

603

in environment [env] *)

604

let type_coreclock env ck id loc =

605

match ck.ck_dec_desc with

606

 Ckdec_any > ()

607

 Ckdec_bool cl >

608

let dummy_id_expr = expr_of_ident id loc in

609

let when_expr =

610

List.fold_left

611

(fun expr (x, l) >

612

{expr_tag = new_tag ();

613

expr_desc= Expr_when (expr,x,l);

614

expr_type = Types.Main.new_var ();

615

expr_clock = Clocks.new_var true;

616

expr_delay = Delay.new_var ();

617

expr_loc=loc;

618

expr_annot = None})

619

dummy_id_expr cl

620

in

621

ignore (type_expr env false false when_expr)

622


623

let rec check_type_declaration loc cty =

624

match cty with

625

 Tydec_clock ty

626

 Tydec_array (_, ty) > check_type_declaration loc ty

627

 Tydec_const tname >

628

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

629

if not (Hashtbl.mem type_table cty)

630

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

631

 _ > ()

632


633

let type_var_decl vd_env env vdecl =

634

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

635

check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;

636

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

637

let type_dim d =

638

begin

639

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

640

Dimension.eval Basic_library.eval_env eval_const d;

641

end in

642

let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in

643


644

let ty_static =

645

if vdecl.var_dec_const

646

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

647

else ty in

648

(match vdecl.var_dec_value with

649

 None > ()

650

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

651

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

652

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

653

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

654

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

655

new_env

656


657

let type_var_decl_list vd_env env l =

658

List.fold_left (type_var_decl vd_env) env l

659


660

let type_of_vlist vars =

661

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

662

type_of_type_list tyl

663


664

let add_vdecl vd_env vdecl =

665

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

666

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

667

else vdecl::vd_env

668


669

let check_vd_env vd_env =

670

ignore (List.fold_left add_vdecl [] vd_env)

671


672

let type_spec env spec =

673

let vd_env = spec.consts @ spec.locals in

674

check_vd_env vd_env;

675

let env = type_var_decl_list ((* this argument seems useless to me, cf TODO at top of the file*) vd_env) env vd_env in

676

(* typing stmts *)

677

let eqs = List.map (fun s > match s with Eq eq > eq  _ > assert false) spec.stmts in

678

let undefined_vars_init =

679

List.fold_left

680

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

681

ISet.empty spec.locals

682

in

683

let _ =

684

List.fold_left

685

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

686

undefined_vars_init

687

eqs

688

in

689


690

(*TODO

691

enrich env locally with locals and consts

692

type each pre/post as a boolean expr

693

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

694

For the moment, returning the provided env

695

*)

696

env

697


698

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

699

location is used for error reports. *)

700

let type_node env nd loc =

701

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

702

let vd_env_ol = nd.node_outputs@nd.node_locals in

703

let vd_env = nd.node_inputs@vd_env_ol in

704

check_vd_env vd_env;

705

let init_env = env in

706

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

707

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

708

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

709

let new_env = Env.overwrite env delta_env in

710

let undefined_vars_init =

711

List.fold_left

712

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

713

ISet.empty vd_env_ol in

714

let undefined_vars =

715

let eqs, auts = get_node_eqs nd in

716

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

717

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

718

in

719

(* Typing asserts *)

720

List.iter (fun assert_ >

721

let assert_expr = assert_.assert_expr in

722

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

723

) nd.node_asserts;

724

(* Typing spec/contracts *)

725

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

726

(* Typing annots *)

727

List.iter (fun annot >

728

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

729

) nd.node_annot;

730


731

(* check that table is empty *)

732

let local_consts = List.fold_left (fun res vdecl > if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in

733

let undefined_vars = ISet.diff undefined_vars local_consts in

734

if (not (ISet.is_empty undefined_vars)) then

735

raise (Error (loc, Undefined_var undefined_vars));

736

let ty_ins = type_of_vlist nd.node_inputs in

737

let ty_outs = type_of_vlist nd.node_outputs in

738

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

739

generalize ty_node;

740

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

741

nd.node_type < Expr_type_hub.export ty_node;

742

Env.add_value env nd.node_id ty_node

743


744

let type_imported_node env nd loc =

745

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

746

check_vd_env vd_env;

747

let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in

748

let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in

749

let new_env = Env.overwrite env delta_env in

750

(* Typing spec *)

751

(match nd.nodei_spec with None > ()  Some spec > ignore (type_spec new_env spec));

752

let ty_ins = type_of_vlist nd.nodei_inputs in

753

let ty_outs = type_of_vlist nd.nodei_outputs in

754

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

755

generalize ty_node;

756

(*

757

if (is_polymorphic ty_node) then

758

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

759

*)

760

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

761

nd.nodei_type < Expr_type_hub.export ty_node;

762

new_env

763


764

let type_top_const env cdecl =

765

let ty = type_const cdecl.const_loc cdecl.const_value in

766

let d =

767

if is_dimension_type ty

768

then dimension_of_const cdecl.const_loc cdecl.const_value

769

else Dimension.mkdim_var () in

770

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

771

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

772

cdecl.const_type < Expr_type_hub.export ty;

773

new_env

774


775

let type_top_consts env clist =

776

List.fold_left type_top_const env clist

777


778

let rec type_top_decl env decl =

779

match decl.top_decl_desc with

780

 Node nd > (

781

try

782

type_node env nd decl.top_decl_loc

783

with Error (loc, err) as exc > (

784

if !Options.global_inline then

785

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

786

Printers.pp_node nd

787

;

788

raise exc)

789

)

790

 ImportedNode nd >

791

type_imported_node env nd decl.top_decl_loc

792

 Const c >

793

type_top_const env c

794

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

795

 Include _  Open _ > env

796


797

let get_type_of_call decl =

798

match decl.top_decl_desc with

799

 Node nd >

800

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

801

type_list_of_type in_typ, type_list_of_type out_typ

802

 ImportedNode nd >

803

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

804

type_list_of_type in_typ, type_list_of_type out_typ

805

 _ > assert false

806


807

let type_prog env decls =

808

try

809

List.fold_left type_top_decl env decls

810

with Failure _ as exc > raise exc

811


812

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

813

original description of dimensions, with constant parameters,

814

instead of unifiable internal variables. *)

815


816

(* The following functions aims at 'unevaluating' dimension

817

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

818

second_order variables with the original static parameters.

819

Once restored in this formulation, dimensions may be

820

meaningfully printed. *)

821

let uneval_vdecl_generics vdecl =

822

if vdecl.var_dec_const

823

then

824

match get_static_value (Expr_type_hub.import vdecl.var_type) with

825

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

826

 Some d > Dimension.uneval vdecl.var_id d

827


828

let uneval_node_generics vdecls =

829

List.iter uneval_vdecl_generics vdecls

830


831

let uneval_spec_generics spec =

832

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

833


834

let uneval_top_generics decl =

835

match decl.top_decl_desc with

836

 Node nd >

837

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

838

 ImportedNode nd >

839

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

840

 Const _  TypeDef _  Open _  Include _

841

> ()

842


843

let uneval_prog_generics prog =

844

List.iter uneval_top_generics prog

845


846

let rec get_imported_symbol decls id =

847

match decls with

848

 [] > assert false

849

 decl::q >

850

(match decl.top_decl_desc with

851

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

852

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

853

 TypeDef _ > get_imported_symbol (consts_of_enum_type decl @ q) id

854

 _ > get_imported_symbol q id)

855


856

let check_env_compat header declared computed =

857

uneval_prog_generics header;

858

Env.iter declared (fun k decl_type_k >

859

let loc = (get_imported_symbol header k).top_decl_loc in

860

let computed_t =

861

instantiate (ref []) (ref [])

862

(try Env.lookup_value computed k

863

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

864

(*Types.print_ty Format.std_formatter decl_type_k;

865

Types.print_ty Format.std_formatter computed_t;*)

866

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

867

)

868


869

let check_typedef_top decl =

870

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

871

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

872

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

873

match decl.top_decl_desc with

874

 TypeDef ty >

875

let owner = decl.top_decl_owner in

876

let itf = decl.top_decl_itf in

877

let decl' =

878

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

879

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

880

let owner' = decl'.top_decl_owner in

881

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

882

let itf' = decl'.top_decl_itf in

883

(match decl'.top_decl_desc with

884

 Const _  Node _  ImportedNode _ > assert false

885

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

886

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

887

 _ > ()

888


889

let check_typedef_compat header =

890

List.iter check_typedef_top header

891

end

892


893

include Make(Types.Main) (struct

894

type type_expr = Types.Main.type_expr

895

let import x = x

896

let export x = x

897

end)

898

(* Local Variables: *)

899

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

900

(* End: *)
