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 s  Const_modeid s >

338

if is_annot then (* Type_predef. *)type_string else (Format.eprintf "Typing string %s outisde of annot scope@.@?" s; 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_contract env c =

673

let vd_env = c.consts @ c.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) c.stmts in

678

let undefined_vars_init =

679

List.fold_left

680

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

681

ISet.empty c.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

c.assume

696

@ c.guarantees

697

@ List.flatten (List.map (fun m > m.ensure @ m.require) c.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

let rec type_spec env spec loc =

708

match spec with

709

 Contract c > type_contract env c

710

 NodeSpec id > env

711


712

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

713

location is used for error reports. *)

714

and type_node env nd loc =

715

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

716

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

717

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

718

let vd_env_ol = if nd.node_iscontract then nd.node_locals else nd.node_outputs@nd.node_locals in

719

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

720

check_vd_env vd_env;

721

let init_env = env in

722

let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in

723

let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in

724

let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in

725

let new_env = Env.overwrite env delta_env in

726

let undefined_vars_init =

727

List.fold_left

728

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

729

ISet.empty vd_env_ol in

730

let undefined_vars =

731

let eqs, auts = get_node_eqs nd in

732

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

733

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

734

in

735

(* Typing asserts *)

736

List.iter (fun assert_ >

737

let assert_expr = assert_.assert_expr in

738

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

739

) nd.node_asserts;

740

(* Typing spec/contracts *)

741

(match nd.node_spec with

742

 None > ()

743

 Some spec > ignore (type_spec new_env spec loc));

744

(* Typing annots *)

745

List.iter (fun annot >

746

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

747

) nd.node_annot;

748


749

(* check that table is empty *)

750

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

751

let undefined_vars = ISet.diff undefined_vars local_consts in

752


753

if (not (ISet.is_empty undefined_vars)) then

754

raise (Error (loc, Undefined_var undefined_vars));

755

let ty_ins = type_of_vlist nd.node_inputs in

756

let ty_outs = type_of_vlist nd.node_outputs in

757

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

758

generalize ty_node;

759

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

760

nd.node_type < Expr_type_hub.export ty_node;

761

Env.add_value env nd.node_id ty_node

762


763

let type_imported_node env nd loc =

764

let vd_env = nd.nodei_inputs@nd.nodei_outputs in

765

check_vd_env vd_env;

766

let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in

767

let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in

768

let new_env = Env.overwrite env delta_env in

769

(* Typing spec *)

770

(match nd.nodei_spec with

771

 None > ()

772

 Some spec > ignore (type_spec new_env spec loc));

773

let ty_ins = type_of_vlist nd.nodei_inputs in

774

let ty_outs = type_of_vlist nd.nodei_outputs in

775

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

776

generalize ty_node;

777

(*

778

if (is_polymorphic ty_node) then

779

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

780

*)

781

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

782

nd.nodei_type < Expr_type_hub.export ty_node;

783

new_env

784


785

let type_top_const env cdecl =

786

let ty = type_const cdecl.const_loc cdecl.const_value in

787

let d =

788

if is_dimension_type ty

789

then dimension_of_const cdecl.const_loc cdecl.const_value

790

else Dimension.mkdim_var () in

791

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

792

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

793

cdecl.const_type < Expr_type_hub.export ty;

794

new_env

795


796

let type_top_consts env clist =

797

List.fold_left type_top_const env clist

798


799

let rec type_top_decl env decl =

800

match decl.top_decl_desc with

801

 Node nd > (

802

try

803

type_node env nd decl.top_decl_loc

804

with Error (loc, err) as exc > (

805

if !Options.global_inline then

806

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

807

Printers.pp_node nd

808

;

809

raise exc)

810

)

811

 ImportedNode nd >

812

type_imported_node env nd decl.top_decl_loc

813

 Const c >

814

type_top_const env c

815

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

816

 Include _  Open _ > env

817


818

let get_type_of_call decl =

819

match decl.top_decl_desc with

820

 Node nd >

821

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

822

type_list_of_type in_typ, type_list_of_type out_typ

823

 ImportedNode nd >

824

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

825

type_list_of_type in_typ, type_list_of_type out_typ

826

 _ > assert false

827


828

let type_prog env decls =

829

try

830

List.fold_left type_top_decl env decls

831

with Failure _ as exc > raise exc

832


833

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

834

original description of dimensions, with constant parameters,

835

instead of unifiable internal variables. *)

836


837

(* The following functions aims at 'unevaluating' dimension

838

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

839

second_order variables with the original static parameters.

840

Once restored in this formulation, dimensions may be

841

meaningfully printed. *)

842

let uneval_vdecl_generics vdecl =

843

if vdecl.var_dec_const

844

then

845

match get_static_value (Expr_type_hub.import vdecl.var_type) with

846

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

847

 Some d > Dimension.uneval vdecl.var_id d

848


849

let uneval_node_generics vdecls =

850

List.iter uneval_vdecl_generics vdecls

851


852

let uneval_spec_generics spec =

853

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

854


855

let uneval_top_generics decl =

856

match decl.top_decl_desc with

857

 Node nd >

858

uneval_node_generics (nd.node_inputs @ nd.node_outputs)

859

 ImportedNode nd >

860

uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)

861

 Const _  TypeDef _  Open _  Include _

862

> ()

863


864

let uneval_prog_generics prog =

865

List.iter uneval_top_generics prog

866


867

let rec get_imported_symbol decls id =

868

match decls with

869

 [] > assert false

870

 decl::q >

871

(match decl.top_decl_desc with

872

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

873

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

874

 TypeDef _ > get_imported_symbol (consts_of_enum_type decl @ q) id

875

 _ > get_imported_symbol q id)

876


877

let check_env_compat header declared computed =

878

uneval_prog_generics header;

879

Env.iter declared (fun k decl_type_k >

880

let top = get_imported_symbol header k in

881

let loc = top.top_decl_loc in

882

try

883

let computed_t = Env.lookup_value computed k in

884

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

885

(*Types.print_ty Format.std_formatter decl_type_k;

886

Types.print_ty Format.std_formatter computed_t;*)

887

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

888

with Not_found >

889

begin

890

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

891

file to provide the same definition. *)

892

match top.top_decl_desc with

893

 Node nd > (

894

match nd.node_spec with

895

 Some (Contract _) > ()

896

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

897

)

898

 _ >

899

raise (Error (loc, Declared_but_undefined k))

900

end

901

)

902


903

let check_typedef_top decl =

904

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

905

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

906

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

907

match decl.top_decl_desc with

908

 TypeDef ty >

909

let owner = decl.top_decl_owner in

910

let itf = decl.top_decl_itf in

911

let decl' =

912

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

913

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

914

let owner' = decl'.top_decl_owner in

915

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

916

let itf' = decl'.top_decl_itf in

917

(match decl'.top_decl_desc with

918

 Const _  Node _  ImportedNode _ > assert false

919

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

920

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

921

 _ > ()

922


923

let check_typedef_compat header =

924

List.iter check_typedef_top header

925

end

926


927

include Make(Types.Main) (struct

928

type type_expr = Types.Main.type_expr

929

let import x = x

930

let export x = x

931

end)

932

(* Local Variables: *)

933

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

934

(* End: *)
