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: except in the add_vdecl, 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

(* Typing each predicate expr *)

690

let type_pred_ee ee : unit=

691

type_subtyping_arg (env, vd_env) (false (* not in main *)) (false (* not a const *)) ee.eexpr_qfexpr type_bool

692

in

693

List.iter type_pred_ee

694

(

695

spec.assume

696

@ spec.guarantees

697

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

698

);

699

(*TODO

700

enrich env locally with locals and consts

701

type each pre/post as a boolean expr

702

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

703

For the moment, returning the provided env

704

*)

705

env

706


707

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

708

location is used for error reports. *)

709

let type_node env nd loc =

710

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

711

let vd_env_ol = nd.node_outputs@nd.node_locals in

712

let vd_env = nd.node_inputs@vd_env_ol in

713

check_vd_env vd_env;

714

let init_env = env in

715

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

716

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

717

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

718

let new_env = Env.overwrite env delta_env in

719

let undefined_vars_init =

720

List.fold_left

721

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

722

ISet.empty vd_env_ol in

723

let undefined_vars =

724

let eqs, auts = get_node_eqs nd in

725

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

726

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

727

in

728

(* Typing asserts *)

729

List.iter (fun assert_ >

730

let assert_expr = assert_.assert_expr in

731

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

732

) nd.node_asserts;

733

(* Typing spec/contracts *)

734

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

735

(* Typing annots *)

736

List.iter (fun annot >

737

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

738

) nd.node_annot;

739


740

(* check that table is empty *)

741

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

742

let undefined_vars = ISet.diff undefined_vars local_consts in

743

if (not (ISet.is_empty undefined_vars)) then

744

raise (Error (loc, Undefined_var undefined_vars));

745

let ty_ins = type_of_vlist nd.node_inputs in

746

let ty_outs = type_of_vlist nd.node_outputs in

747

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

748

generalize ty_node;

749

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

750

nd.node_type < Expr_type_hub.export ty_node;

751

Env.add_value env nd.node_id ty_node

752


753

let type_imported_node env nd loc =

754

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

755

check_vd_env vd_env;

756

let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in

757

let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in

758

let new_env = Env.overwrite env delta_env in

759

(* Typing spec *)

760

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

761

let ty_ins = type_of_vlist nd.nodei_inputs in

762

let ty_outs = type_of_vlist nd.nodei_outputs in

763

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

764

generalize ty_node;

765

(*

766

if (is_polymorphic ty_node) then

767

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

768

*)

769

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

770

nd.nodei_type < Expr_type_hub.export ty_node;

771

new_env

772


773

let type_top_const env cdecl =

774

let ty = type_const cdecl.const_loc cdecl.const_value in

775

let d =

776

if is_dimension_type ty

777

then dimension_of_const cdecl.const_loc cdecl.const_value

778

else Dimension.mkdim_var () in

779

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

780

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

781

cdecl.const_type < Expr_type_hub.export ty;

782

new_env

783


784

let type_top_consts env clist =

785

List.fold_left type_top_const env clist

786


787

let rec type_top_decl env decl =

788

match decl.top_decl_desc with

789

 Node nd > (

790

try

791

type_node env nd decl.top_decl_loc

792

with Error (loc, err) as exc > (

793

if !Options.global_inline then

794

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

795

Printers.pp_node nd

796

;

797

raise exc)

798

)

799

 ImportedNode nd >

800

type_imported_node env nd decl.top_decl_loc

801

 Const c >

802

type_top_const env c

803

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

804

 Include _  Open _ > env

805


806

let get_type_of_call decl =

807

match decl.top_decl_desc with

808

 Node nd >

809

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

810

type_list_of_type in_typ, type_list_of_type out_typ

811

 ImportedNode nd >

812

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

813

type_list_of_type in_typ, type_list_of_type out_typ

814

 _ > assert false

815


816

let type_prog env decls =

817

try

818

List.fold_left type_top_decl env decls

819

with Failure _ as exc > raise exc

820


821

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

822

original description of dimensions, with constant parameters,

823

instead of unifiable internal variables. *)

824


825

(* The following functions aims at 'unevaluating' dimension

826

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

827

second_order variables with the original static parameters.

828

Once restored in this formulation, dimensions may be

829

meaningfully printed. *)

830

let uneval_vdecl_generics vdecl =

831

if vdecl.var_dec_const

832

then

833

match get_static_value (Expr_type_hub.import vdecl.var_type) with

834

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

835

 Some d > Dimension.uneval vdecl.var_id d

836


837

let uneval_node_generics vdecls =

838

List.iter uneval_vdecl_generics vdecls

839


840

let uneval_spec_generics spec =

841

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

842


843

let uneval_top_generics decl =

844

match decl.top_decl_desc with

845

 Node nd >

846

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

847

 ImportedNode nd >

848

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

849

 Const _  TypeDef _  Open _  Include _

850

> ()

851


852

let uneval_prog_generics prog =

853

List.iter uneval_top_generics prog

854


855

let rec get_imported_symbol decls id =

856

match decls with

857

 [] > assert false

858

 decl::q >

859

(match decl.top_decl_desc with

860

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

861

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

862

 TypeDef _ > get_imported_symbol (consts_of_enum_type decl @ q) id

863

 _ > get_imported_symbol q id)

864


865

let check_env_compat header declared computed =

866

uneval_prog_generics header;

867

Env.iter declared (fun k decl_type_k >

868

let loc = (get_imported_symbol header k).top_decl_loc in

869

let computed_t =

870

instantiate (ref []) (ref [])

871

(try Env.lookup_value computed k

872

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

873

(*Types.print_ty Format.std_formatter decl_type_k;

874

Types.print_ty Format.std_formatter computed_t;*)

875

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

876

)

877


878

let check_typedef_top decl =

879

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

880

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

881

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

882

match decl.top_decl_desc with

883

 TypeDef ty >

884

let owner = decl.top_decl_owner in

885

let itf = decl.top_decl_itf in

886

let decl' =

887

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

888

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

889

let owner' = decl'.top_decl_owner in

890

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

891

let itf' = decl'.top_decl_itf in

892

(match decl'.top_decl_desc with

893

 Const _  Node _  ImportedNode _ > assert false

894

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

895

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

896

 _ > ()

897


898

let check_typedef_compat header =

899

List.iter check_typedef_top header

900

end

901


902

include Make(Types.Main) (struct

903

type type_expr = Types.Main.type_expr

904

let import x = x

905

let export x = x

906

end)

907

(* Local Variables: *)

908

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

909

(* End: *)
