1

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

2

(* *)

3

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

4

(* Copyright 2012   ONERA  CNRS  INPT *)

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

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

11


12

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

13

unification. *)

14


15

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

16

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

17

redefinition allowed. *)

18


19

open Utils

20


21

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

22

yet this makes notations far lighter.*)

23

open Corelang

24

open Init

25

open Format

26


27

(** [occurs tvar ty] returns true if the type variable [tvar] occurs in type

28

[ty]. False otherwise. *)

29

let rec occurs tvar ty =

30

let ty = repr ty in

31

match ty.tdesc with

32

 Ivar >

33

ty = tvar

34

 Iarrow (t1, t2) >

35

occurs tvar t1  occurs tvar t2

36

 Ituple tl >

37

List.exists (occurs tvar) tl

38

 Ilink t >

39

occurs tvar t

40

 Isucc t >

41

occurs tvar t

42

 Iunivar >

43

false

44


45

(* Generalize by sideeffects *)

46


47

(** Promote monomorphic type variables to polymorphic type variables. *)

48

let rec generalize ty =

49

match ty.tdesc with

50

 Ivar >

51

(* No scopes, always generalize *)

52

ty.idesc < Iunivar

53

 Iarrow (t1, t2) >

54

generalize t1;

55

generalize t2

56

 Ituple tlist >

57

List.iter generalize tlist

58

 Ilink t >

59

generalize t

60

 Isucc t >

61

generalize t

62

 Tunivar >

63

()

64


65

(** Downgrade polymorphic type variables to monomorphic type variables *)

66

let rec instanciate inst_vars ty =

67

let ty = repr ty in

68

match ty.idesc with

69

 Ivar >

70

ty

71

 Iarrow (t1, t2) >

72

{

73

ty with

74

idesc = Iarrow (instanciate inst_vars t1, instanciate inst_vars t2);

75

}

76

 Ituple tlist >

77

{ ty with idesc = Ituple (List.map (instanciate inst_vars) tlist) }

78

 Isucc t >

79

(* should not happen *)

80

{ ty with idesc = Isucc (instanciate inst_vars t) }

81

 Ilink t >

82

(* should not happen *)

83

{ ty with idesc = Ilink (instanciate inst_vars t) }

84

 Iunivar > (

85

try List.assoc ty.iid !inst_vars

86

with Not_found >

87

let var = new_var () in

88

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

89

var)

90


91

(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify (t1,t2)] if the

92

types are not unifiable.*)

93


94

(* Standard destructive unification *)

95

(* may loop for omega types *)

96

let rec unify t1 t2 =

97

let t1 = repr t1 in

98

let t2 = repr t2 in

99

if t1 = t2 then ()

100

else

101

(* No type abbreviations resolution for now *)

102

match t1.idesc, t2.idesc with

103

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

104

 Ivar, Ivar >

105

if t1.iid < t2.iid then t2.idesc < Ilink t1 else t1.idesc < Ilink t2

106

 Ivar, _ when not (occurs t1 t2) >

107

t1.idesc < Ilink t2

108

 _, Ivar when not (occurs t2 t1) >

109

t2.idesc < Ilink t1

110

 Isucc t1, Isucc t1' >

111

unify t1 t1'

112

 Iarrow (t1, t2), Iarrow (t1', t2') >

113

unify t1 t1';

114

unify t2 t2'

115

 Ituple tlist1, Ituple tlist2 >

116

if List.length tlist1 <> List.length tlist2 then raise (Unify (t1, t2))

117

else List.iter2 unify tlist1 tlist2

118

 Iunivar, _  _, Iunivar >

119

()

120

 _, _ >

121

raise (Unify (t1, t2))

122


123

let init_of_const c = Init_predef.init_zero

124


125

let rec init_expect env in_main expr ty =

126

let texpr = init_expr env in_main expr in

127

try unify texpr ty

128

with Unify (t1, t2) > raise (Error (expr.expr_loc, Init_clash (t1, t2)))

129


130

and init_ident env in_main id loc = init_expr env in_main (expr_of_ident id loc)

131


132

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

133

and init_expr env in_main expr =

134

match expr.expr_desc with

135

 Expr_const c >

136

let ty = init_of_const c in

137

expr.expr_init < ty;

138

ty

139

 Expr_ident v >

140

let tyv =

141

try Env.lookup_value env v

142

with Not_found > raise (Error (expr.expr_loc, Unbound_value v))

143

in

144

let ty = instanciate (ref []) tyv in

145

expr.expr_init < ty;

146

ty

147

 Expr_tuple elist >

148

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

149

expr.expr_init < ty;

150

ty

151

 Expr_appl (id, args, r) >

152

(match r with

153

 None >

154

()

155

 Some x >

156

let expr_x = expr_of_ident x expr.expr_loc in

157

init_expect env in_main expr_x Init_predef.init_zero);

158

let tfun = type_ident env in_main id expr.expr_loc in

159

let tins, touts = split_arrow tfun in

160

type_expect env in_main args tins;

161

expr.expr_type < touts;

162

touts

163

 Expr_arrow (e1, e2) >

164

let ty = type_expr env in_main e1 in

165

type_expect env in_main e2 ty;

166

expr.expr_type < ty;

167

ty

168

 Expr_fby (init, e) >

169

let ty = type_of_const init in

170

type_expect env in_main e ty;

171

expr.expr_type < ty;

172

ty

173

 Expr_concat (hd, e) >

174

let ty = type_of_const hd in

175

type_expect env in_main e ty;

176

expr.expr_type < ty;

177

ty

178

 Expr_tail e >

179

let ty = type_expr env in_main e in

180

expr.expr_type < ty;

181

ty

182

 Expr_pre e >

183

let ty = type_expr env in_main e in

184

expr.expr_type < ty;

185

ty

186

 Expr_when (e1, c)  Expr_whennot (e1, c) >

187

let expr_c = expr_of_ident c expr.expr_loc in

188

type_expect env in_main expr_c Type_predef.type_bool;

189

let tlarg = type_expr env in_main e1 in

190

expr.expr_type < tlarg;

191

tlarg

192

 Expr_merge (c, e2, e3) >

193

let expr_c = expr_of_ident c expr.expr_loc in

194

type_expect env in_main expr_c Type_predef.type_bool;

195

let te2 = type_expr env in_main e2 in

196

type_expect env in_main e3 te2;

197

expr.expr_type < te2;

198

te2

199

 Expr_uclock (e, k)  Expr_dclock (e, k) >

200

let ty = type_expr env in_main e in

201

expr.expr_type < ty;

202

ty

203

 Expr_phclock (e, q) >

204

let ty = type_expr env in_main e in

205

expr.expr_type < ty;

206

ty

207


208

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

209

let type_eq env in_main undefined_vars eq =

210

(* Check multiple variable definitions *)

211

let define_var id uvars =

212

try

213

ignore (IMap.find id uvars);

214

IMap.remove id uvars

215

with Not_found > raise (Error (eq.eq_loc, Already_defined id))

216

in

217

let undefined_vars =

218

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

219

in

220

(* Type lhs *)

221

let get_value_type id =

222

try Env.lookup_value env id

223

with Not_found > raise (Error (eq.eq_loc, Unbound_value id))

224

in

225

let tyl_lhs = List.map get_value_type eq.eq_lhs in

226

let ty_lhs = type_of_type_list tyl_lhs in

227

(* Type rhs *)

228

type_expect env in_main eq.eq_rhs ty_lhs;

229

undefined_vars

230


231

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

232

let type_coretype cty =

233

match cty with

234

 Tydec_any >

235

new_var ()

236

 Tydec_int >

237

Type_predef.type_int

238

 Tydec_real >

239

Type_predef.type_real

240

 Tydec_float >

241

Type_predef.type_real

242

 Tydec_bool >

243

Type_predef.type_bool

244

 Tydec_clock >

245

Type_predef.type_clock

246


247

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

248

environment [env] *)

249

let type_coreclock env ck id loc =

250

match ck.ck_dec_desc with

251

 Ckdec_any  Ckdec_pclock (_, _) >

252

()

253

 Ckdec_bool cl >

254

let dummy_id_expr = expr_of_ident id loc in

255

let when_expr =

256

List.fold_left

257

(fun expr c >

258

match c with

259

 Wtrue id >

260

{

261

expr_tag = new_tag ();

262

expr_desc = Expr_when (expr, id);

263

expr_type = new_var ();

264

expr_clock = Clocks.new_var true;

265

expr_loc = loc;

266

}

267

 Wfalse id >

268

{

269

expr_tag = new_tag ();

270

expr_desc = Expr_whennot (expr, id);

271

expr_type = new_var ();

272

expr_clock = Clocks.new_var true;

273

expr_loc = loc;

274

})

275

dummy_id_expr cl

276

in

277

ignore (type_expr env false when_expr)

278


279

let type_var_decl env vdecl =

280

if Env.exists_value env vdecl.var_id then

281

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

282

else

283

let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in

284

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

285

type_coreclock new_env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;

286

vdecl.var_type < ty;

287

new_env

288


289

let type_var_decl_list env l = List.fold_left type_var_decl env l

290


291

let type_of_vlist vars =

292

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

293

type_of_type_list tyl

294


295

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

296

used for error reports. *)

297

let type_node env nd loc =

298

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

299

let delta_env = type_var_decl_list IMap.empty nd.node_inputs in

300

let delta_env = type_var_decl_list delta_env nd.node_outputs in

301

let delta_env = type_var_decl_list delta_env nd.node_locals in

302

let new_env = Env.overwrite env delta_env in

303

let undefined_vars_init =

304

List.fold_left

305

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

306

IMap.empty

307

(nd.node_outputs @ nd.node_locals)

308

in

309

let undefined_vars =

310

List.fold_left (type_eq new_env is_main) undefined_vars_init nd.node_eqs

311

in

312

(* check that table is empty *)

313

if not (IMap.is_empty undefined_vars) then

314

raise (Error (loc, Undefined_var undefined_vars));

315

let ty_ins = type_of_vlist nd.node_inputs in

316

let ty_outs = type_of_vlist nd.node_outputs in

317

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

318

generalize ty_node;

319

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

320

nd.node_type < ty_node;

321

Env.add_value env nd.node_id ty_node

322


323

let type_imported_node env nd loc =

324

let new_env = type_var_decl_list env nd.nodei_inputs in

325

ignore (type_var_decl_list new_env nd.nodei_outputs);

326

let ty_ins = type_of_vlist nd.nodei_inputs in

327

let ty_outs = type_of_vlist nd.nodei_outputs in

328

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

329

generalize ty_node;

330

if is_polymorphic ty_node then

331

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

332

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

333

nd.nodei_type < ty_node;

334

new_env

335


336

let type_top_decl env decl =

337

match decl.top_decl_desc with

338

 Node nd >

339

type_node env nd decl.top_decl_loc

340

 ImportedNode nd >

341

type_imported_node env nd decl.top_decl_loc

342

 SensorDecl _  ActuatorDecl _  Consts _ >

343

env

344


345

let type_top_consts env decl =

346

match decl.top_decl_desc with

347

 Consts clist >

348

List.fold_left

349

(fun env (id, c) >

350

let ty = type_of_const c in

351

Env.add_value env id ty)

352

env clist

353

 Node _  ImportedNode _  SensorDecl _  ActuatorDecl _ >

354

env

355


356

let type_prog env decls =

357

let new_env = List.fold_left type_top_consts env decls in

358

ignore (List.fold_left type_top_decl new_env decls)

359


360

(* Local Variables: *)

361

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

362

(* End: *)
