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

16

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

17

identifier redefinition allowed. *)

18


19

open Utils

20

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

21

overwritten, yet this makes notations far lighter.*)

22

open Corelang

23

open Init

24

open Format

25


26

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

27

type [ty]. False otherwise. *)

28

let rec occurs tvar ty =

29

let ty = repr ty in

30

match ty.tdesc with

31

 Ivar > ty=tvar

32

 Iarrow (t1, t2) >

33

(occurs tvar t1)  (occurs tvar t2)

34

 Ituple tl >

35

List.exists (occurs tvar) tl

36

 Ilink t > occurs tvar t

37

 Isucc t > occurs tvar t

38

 Iunivar > false

39


40

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

41

(* Generalize by sideeffects *)

42

let rec generalize ty =

43

match ty.tdesc with

44

 Ivar >

45

(* No scopes, always generalize *)

46

ty.idesc < Iunivar

47

 Iarrow (t1,t2) >

48

generalize t1; generalize t2

49

 Ituple tlist >

50

List.iter generalize tlist

51

 Ilink t >

52

generalize t

53

 Isucc t >

54

generalize t

55

 Tunivar > ()

56


57

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

58

let rec instanciate inst_vars ty =

59

let ty = repr ty in

60

match ty.idesc with

61

 Ivar > ty

62

 Iarrow (t1,t2) >

63

{ty with idesc =

64

Iarrow ((instanciate inst_vars t1), (instanciate inst_vars t2))}

65

 Ituple tlist >

66

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

67

 Isucc t >

68

(* should not happen *)

69

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

70

 Ilink t >

71

(* should not happen *)

72

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

73

 Iunivar >

74

try

75

List.assoc ty.iid !inst_vars

76

with Not_found >

77

let var = new_var () in

78

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

79

var

80


81

(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify

82

(t1,t2)] if the types are not unifiable.*)

83


84

(* Standard destructive unification *)

85

(* may loop for omega types *)

86

let rec unify t1 t2 =

87

let t1 = repr t1 in

88

let t2 = repr t2 in

89

if t1=t2 then

90

()

91

else

92

(* No type abbreviations resolution for now *)

93

match t1.idesc,t2.idesc with

94

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

95

 Ivar, Ivar >

96

if t1.iid < t2.iid then

97

t2.idesc < Ilink t1

98

else

99

t1.idesc < Ilink t2

100

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

101

t1.idesc < Ilink t2

102

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

103

t2.idesc < Ilink t1

104

 Isucc t1, Isucc t1' > unify t1 t1'

105

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

106

unify t1 t1'; unify t2 t2'

107

 Ituple tlist1, Ituple tlist2 >

108

if (List.length tlist1) <> (List.length tlist2) then

109

raise (Unify (t1, t2))

110

else

111

List.iter2 unify tlist1 tlist2

112

 Iunivar,_  _, Iunivar >

113

()

114

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

115


116

let init_of_const c =

117

Init_predef.init_zero

118


119

let rec init_expect env in_main expr ty =

120

let texpr = init_expr env in_main expr in

121

try

122

unify texpr ty

123

with Unify (t1,t2) >

124

raise (Error (expr.expr_loc, Init_clash (t1,t2)))

125


126

and init_ident env in_main id loc =

127

init_expr env in_main (expr_of_ident id loc)

128


129

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

130

[env]. *)

131

and init_expr env in_main expr =

132

match expr.expr_desc with

133

 Expr_const c >

134

let ty = init_of_const c in

135

expr.expr_init < ty;

136

ty

137

 Expr_ident v >

138

let tyv =

139

try

140

Env.lookup_value env v

141

with Not_found >

142

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

 Some x > let expr_x = expr_of_ident x expr.expr_loc in

155

init_expect env in_main expr_x Init_predef.init_zero);

156

let tfun = type_ident env in_main id expr.expr_loc in

157

let tins,touts= split_arrow tfun in

158

type_expect env in_main args tins;

159

expr.expr_type < touts;

160

touts

161

 Expr_arrow (e1,e2) >

162

let ty = type_expr env in_main e1 in

163

type_expect env in_main e2 ty;

164

expr.expr_type < ty;

165

ty

166

 Expr_fby (init,e) >

167

let ty = type_of_const init in

168

type_expect env in_main e ty;

169

expr.expr_type < ty;

170

ty

171

 Expr_concat (hd,e) >

172

let ty = type_of_const hd in

173

type_expect env in_main e ty;

174

expr.expr_type < ty;

175

ty

176

 Expr_tail e >

177

let ty = type_expr env in_main e in

178

expr.expr_type < ty;

179

ty

180

 Expr_pre e >

181

let ty = type_expr env in_main e in

182

expr.expr_type < ty;

183

ty

184

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

185

let expr_c = expr_of_ident c expr.expr_loc in

186

type_expect env in_main expr_c Type_predef.type_bool;

187

let tlarg = type_expr env in_main e1 in

188

expr.expr_type < tlarg;

189

tlarg

190

 Expr_merge (c,e2,e3) >

191

let expr_c = expr_of_ident c expr.expr_loc in

192

type_expect env in_main expr_c Type_predef.type_bool;

193

let te2 = type_expr env in_main e2 in

194

type_expect env in_main e3 te2;

195

expr.expr_type < te2;

196

te2

197

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

198

let ty = type_expr env in_main e in

199

expr.expr_type < ty;

200

ty

201

 Expr_phclock (e,q) >

202

let ty = type_expr env in_main e in

203

expr.expr_type < ty;

204

ty

205


206

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

207

let type_eq env in_main undefined_vars eq =

208

(* Check multiple variable definitions *)

209

let define_var id uvars =

210

try

211

ignore(IMap.find id uvars);

212

IMap.remove id uvars

213

with Not_found >

214

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

215

in

216

let undefined_vars =

217

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

218

(* Type lhs *)

219

let get_value_type id =

220

try

221

Env.lookup_value env id

222

with Not_found >

223

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 > new_var ()

235

 Tydec_int > Type_predef.type_int

236

 Tydec_real > Type_predef.type_real

237

 Tydec_float > Type_predef.type_real

238

 Tydec_bool > Type_predef.type_bool

239

 Tydec_clock > Type_predef.type_clock

240


241

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

242

in environment [env] *)

243

let type_coreclock env ck id loc =

244

match ck.ck_dec_desc with

245

 Ckdec_any  Ckdec_pclock (_,_) > ()

246

 Ckdec_bool cl >

247

let dummy_id_expr = expr_of_ident id loc in

248

let when_expr =

249

List.fold_left

250

(fun expr c >

251

match c with

252

 Wtrue id >

253

{expr_tag = new_tag ();

254

expr_desc=Expr_when (expr,id);

255

expr_type = new_var ();

256

expr_clock = Clocks.new_var true;

257

expr_loc=loc}

258

 Wfalse id >

259

{expr_tag = new_tag ();

260

expr_desc=Expr_whennot (expr,id);

261

expr_type = new_var ();

262

expr_clock = Clocks.new_var true;

263

expr_loc=loc})

264

dummy_id_expr cl

265

in

266

ignore (type_expr env false when_expr)

267


268

let type_var_decl env vdecl =

269

if (Env.exists_value env vdecl.var_id) then

270

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

271

else

272

let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in

273

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

274

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

275

vdecl.var_type < ty;

276

new_env

277


278

let type_var_decl_list env l =

279

List.fold_left type_var_decl env l

280


281

let type_of_vlist vars =

282

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

283

type_of_type_list tyl

284


285

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

286

location is used for error reports. *)

287

let type_node env nd loc =

288

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

289

let delta_env = type_var_decl_list IMap.empty nd.node_inputs in

290

let delta_env = type_var_decl_list delta_env nd.node_outputs in

291

let delta_env = type_var_decl_list delta_env nd.node_locals in

292

let new_env = Env.overwrite env delta_env in

293

let undefined_vars_init =

294

List.fold_left

295

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

296

IMap.empty (nd.node_outputs@nd.node_locals) in

297

let undefined_vars =

298

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

299

in

300

(* check that table is empty *)

301

if (not (IMap.is_empty undefined_vars)) then

302

raise (Error (loc,Undefined_var undefined_vars));

303

let ty_ins = type_of_vlist nd.node_inputs in

304

let ty_outs = type_of_vlist nd.node_outputs in

305

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

306

generalize ty_node;

307

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

308

nd.node_type < ty_node;

309

Env.add_value env nd.node_id ty_node

310


311

let type_imported_node env nd loc =

312

let new_env = type_var_decl_list env nd.nodei_inputs in

313

ignore(type_var_decl_list new_env nd.nodei_outputs);

314

let ty_ins = type_of_vlist nd.nodei_inputs in

315

let ty_outs = type_of_vlist nd.nodei_outputs in

316

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

317

generalize ty_node;

318

if (is_polymorphic ty_node) then

319

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

320

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

321

nd.nodei_type < ty_node;

322

new_env

323


324

let type_top_decl env decl =

325

match decl.top_decl_desc with

326

 Node nd >

327

type_node env nd decl.top_decl_loc

328

 ImportedNode nd >

329

type_imported_node env nd decl.top_decl_loc

330

 SensorDecl _  ActuatorDecl _  Consts _ > env

331


332

let type_top_consts env decl =

333

match decl.top_decl_desc with

334

 Consts clist >

335

List.fold_left (fun env (id, c) >

336

let ty = type_of_const c in

337

Env.add_value env id ty

338

) env clist

339

 Node _  ImportedNode _  SensorDecl _  ActuatorDecl _ > env

340


341

let type_prog env decls =

342

let new_env = List.fold_left type_top_consts env decls in

343

ignore(List.fold_left type_top_decl new_env decls)

344


345

(* Local Variables: *)

346

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

347

(* End: *)
