Revision ca7ff3f7
Added by LĂ©lio Brun over 1 year ago
src/typing.ml  

6  6 
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) 
7  7 
(* under the terms of the GNU Lesser General Public License *) 
8  8 
(* version 2.1. *) 
9 
(* *)


9 
(* *) 

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


11 
(* *) 

12  12 
(********************************************************************) 
13  13  
14  14 
(** Main typing module. Classic inference algorithm with destructive 
15  15 
unification. *) 
16  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. *) 

17 
let debug _fmt _args = () 

18  
19 
(* Format.eprintf "%a" *) 

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

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

22 
redefinition allowed. *) 

21  23  
22  24 
open Utils 
23 
(* Yes, opening both modules is dirty as some type names will be 

24 
overwritten, yet this makes notations far lighter.*) 

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

27 
yet this makes notations far lighter.*) 

25  28 
open Lustre_types 
26  29 
open Corelang 
27  30  
31 
(* TODO general remark: except in the add_vdecl, it seems to me that all the 

32 
pairs (env, vd_env) should be replace with just env, since vd_env is never 

33 
used and the env element is always extract with a fst *) 

34  
35 
module type EXPR_TYPE_HUB = sig 

36 
type type_expr 

28  37  
29 
(* TODO general remark: except in the add_vdecl, it seems to me that 

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

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

32 
fst *) 

38 
val import : Types.Main.type_expr > type_expr 

33  39  
34 


35 
module type EXPR_TYPE_HUB = 

36 
sig 

37 
type type_expr 

38 
val import: Types.Main.type_expr > type_expr 

39 
val export: type_expr > Types.Main.type_expr 

40 
val export : type_expr > Types.Main.type_expr 

40  41 
end 
41  42  
42 
module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) = 

43 
struct 

44  
45 
module TP = Type_predef.Make (T) 

46 
include TP 

47 


48 
let pp_typing_env fmt env = 

49 
Env.pp_env print_ty fmt env 

50  
51 
(****************************************************************) 

52 
(* Generic functions: occurs, instantiate and generalize *) 

53 
(****************************************************************) 

54 


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

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

57 
let rec occurs tvar ty = 

58 
let ty = repr ty in 

59 
match type_desc ty with 

60 
 Tvar > ty=tvar 

61 
 Tarrow (t1, t2) > 

62 
(occurs tvar t1)  (occurs tvar t2) 

63 
 Ttuple tl > 

64 
List.exists (occurs tvar) tl 

65 
 Tstruct fl > 

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

67 
 Tarray (_, t) 

68 
 Tstatic (_, t) 

69 
 Tclock t 

70 
 Tlink t > occurs tvar t 

71 
 Tenum _  Tconst _  Tunivar  Tbasic _ > false 

72  
73 
(** Promote monomorphic type variables to polymorphic type 

74 
variables. *) 

75 
(* Generalize by sideeffects *) 

76 
let rec generalize ty = 

77 
match type_desc ty with 

78 
 Tvar > 

79 
(* No scopes, always generalize *) 

80 
ty.tdesc < Tunivar 

81 
 Tarrow (t1,t2) > 

82 
generalize t1; generalize t2 

83 
 Ttuple tl > 

84 
List.iter generalize tl 

85 
 Tstruct fl > 

86 
List.iter (fun (_, t) > generalize t) fl 

87 
 Tstatic (d, t) 

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

89 
 Tclock t 

90 
 Tlink t > 

91 
generalize t 

92 
 Tenum _  Tconst _  Tunivar  Tbasic _ > () 

93  
94 
(** Downgrade polymorphic type variables to monomorphic type 

95 
variables *) 

96 
let rec instantiate inst_vars inst_dim_vars ty = 

97 
let ty = repr ty in 

98 
match ty.tdesc with 

99 
 Tenum _  Tconst _  Tvar  Tbasic _ > ty 

100 
 Tarrow (t1,t2) > 

101 
{ty with tdesc = 

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

103 
 Ttuple tlist > 

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

105 
 Tstruct flist > 

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

107 
 Tclock t > 

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

109 
 Tstatic (d, t) > 

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

111 
 Tarray (d, t) > 

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

113 
 Tlink t > 

114 
(* should not happen *) 

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

116 
 Tunivar > 

117 
try 

118 
List.assoc ty.tid !inst_vars 

119 
with Not_found > 

120 
let var = new_var () in 

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

122 
var 

123  
124  
125  
126 
let basic_coretype_type t = 

127 
if is_real_type t then Tydec_real else 

128 
if is_int_type t then Tydec_int else 

129 
if is_bool_type t then Tydec_bool else 

130 
assert false 

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

133 
let rec type_coretype type_dim cty = 

134 
match (*get_repr_type*) cty with 

135 
 Tydec_any > new_var () 

136 
 Tydec_int > type_int 

137 
 Tydec_real > (* Type_predef. *)type_real 

138 
(*  Tydec_float > Type_predef.type_real *) 

139 
 Tydec_bool > (* Type_predef. *)type_bool 

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

141 
 Tydec_const c > (* Type_predef. *)type_const c 

142 
 Tydec_enum tl > (* Type_predef. *)type_enum tl 

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

144 
 Tydec_array (d, ty) > 

145 
begin 

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

147 
type_dim d; 

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

149 
end 

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

152 
let rec coretype_type ty = 

153 
match (repr ty).tdesc with 

154 
 Tvar > Tydec_any 

155 
 Tbasic _ > basic_coretype_type ty 

156 
 Tconst c > Tydec_const c 

157 
 Tclock t > Tydec_clock (coretype_type t) 

158 
 Tenum tl > Tydec_enum tl 

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

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

161 
 Tstatic (_, t) > coretype_type t 

162 
 _ > assert false 

163  
164 
let get_coretype_definition tname = 

165 
try 

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

167 
match top.top_decl_desc with 

168 
 TypeDef tdef > tdef.tydef_desc 

169 
 _ > assert false 

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

171  
172 
let get_type_definition tname = 

173 
type_coretype (fun _ > ()) (get_coretype_definition tname) 

174  
175 
(* Equality on ground types only *) 

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

177 
let rec eq_ground t1 t2 = 

43 
module Make 

44 
(T : Types.S) 

45 
(Expr_type_hub : EXPR_TYPE_HUB with type type_expr = T.type_expr) = 

46 
struct 

47 
module TP = Type_predef.Make (T) 

48 
include TP 

49  
50 
let pp_typing_env fmt env = 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] occurs in type 

57 
[ty]. False otherwise. *) 

58 
let rec occurs tvar ty = 

59 
let ty = repr ty in 

60 
match type_desc ty with 

61 
 Tvar > 

62 
ty = tvar 

63 
 Tarrow (t1, t2) > 

64 
occurs tvar t1  occurs tvar t2 

65 
 Ttuple tl > 

66 
List.exists (occurs tvar) tl 

67 
 Tstruct fl > 

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

69 
 Tarray (_, t)  Tstatic (_, t)  Tclock t  Tlink t > 

70 
occurs tvar t 

71 
 Tenum _  Tconst _  Tunivar  Tbasic _ > 

72 
false 

73  
74 
(* Generalize by sideeffects *) 

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

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; 

84 
generalize t2 

85 
 Ttuple tl > 

86 
List.iter generalize tl 

87 
 Tstruct fl > 

88 
List.iter (fun (_, t) > generalize t) fl 

89 
 Tstatic (d, t)  Tarray (d, t) > 

90 
Dimension.generalize d; 

91 
generalize t 

92 
 Tclock t  Tlink t > 

93 
generalize t 

94 
 Tenum _  Tconst _  Tunivar  Tbasic _ > 

95 
() 

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

98 
let rec instantiate inst_vars inst_dim_vars ty = 

99 
let ty = repr ty in 

100 
match ty.tdesc with 

101 
 Tenum _  Tconst _  Tvar  Tbasic _ > 

102 
ty 

103 
 Tarrow (t1, t2) > 

104 
{ 

105 
ty with 

106 
tdesc = 

107 
Tarrow 

108 
( instantiate inst_vars inst_dim_vars t1, 

109 
instantiate inst_vars inst_dim_vars t2 ); 

110 
} 

111 
 Ttuple tlist > 

112 
{ 

113 
ty with 

114 
tdesc = Ttuple (List.map (instantiate inst_vars inst_dim_vars) tlist); 

115 
} 

116 
 Tstruct flist > 

117 
{ 

118 
ty with 

119 
tdesc = 

120 
Tstruct 

121 
(List.map 

122 
(fun (f, t) > f, instantiate inst_vars inst_dim_vars t) 

123 
flist); 

124 
} 

125 
 Tclock t > 

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

127 
 Tstatic (d, t) > 

128 
{ 

129 
ty with 

130 
tdesc = 

131 
Tstatic 

132 
( Dimension.instantiate inst_dim_vars d, 

133 
instantiate inst_vars inst_dim_vars t ); 

134 
} 

135 
 Tarray (d, t) > 

136 
{ 

137 
ty with 

138 
tdesc = 

139 
Tarray 

140 
( Dimension.instantiate inst_dim_vars d, 

141 
instantiate inst_vars inst_dim_vars t ); 

142 
} 

143 
 Tlink t > 

144 
(* should not happen *) 

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

146 
 Tunivar > ( 

147 
try List.assoc ty.tid !inst_vars 

148 
with Not_found > 

149 
let var = new_var () in 

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

151 
var) 

152  
153 
let basic_coretype_type t = 

154 
if is_real_type t then Tydec_real 

155 
else if is_int_type t then Tydec_int 

156 
else if is_bool_type t then Tydec_bool 

157 
else assert false 

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

160 
let rec type_coretype type_dim cty = 

161 
match (*get_repr_type*) 

162 
cty with 

163 
 Tydec_any > 

164 
new_var () 

165 
 Tydec_int > 

166 
type_int 

167 
 Tydec_real > 

168 
(* Type_predef. *) 

169 
type_real 

170 
(*  Tydec_float > Type_predef.type_real *) 

171 
 Tydec_bool > 

172 
(* Type_predef. *) 

173 
type_bool 

174 
 Tydec_clock ty > 

175 
(* Type_predef. *) 

176 
type_clock (type_coretype type_dim ty) 

177 
 Tydec_const c > 

178 
(* Type_predef. *) 

179 
type_const c 

180 
 Tydec_enum tl > 

181 
(* Type_predef. *) 

182 
type_enum tl 

183 
 Tydec_struct fl > 

184 
(* Type_predef. *) 

185 
type_struct (List.map (fun (f, ty) > f, type_coretype type_dim ty) fl) 

186 
 Tydec_array (d, ty) > 

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

188 
type_dim d; 

189 
(* Type_predef. *) 

190 
type_array d (type_coretype type_dim ty) 

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

193 
let rec coretype_type ty = 

194 
match (repr ty).tdesc with 

195 
 Tvar > 

196 
Tydec_any 

197 
 Tbasic _ > 

198 
basic_coretype_type ty 

199 
 Tconst c > 

200 
Tydec_const c 

201 
 Tclock t > 

202 
Tydec_clock (coretype_type t) 

203 
 Tenum tl > 

204 
Tydec_enum tl 

205 
 Tstruct fl > 

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

207 
 Tarray (d, t) > 

208 
Tydec_array (d, coretype_type t) 

209 
 Tstatic (_, t) > 

210 
coretype_type t 

211 
 _ > 

212 
assert false 

213  
214 
let get_coretype_definition tname = 

215 
try 

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

217 
match top.top_decl_desc with 

218 
 TypeDef tdef > 

219 
tdef.tydef_desc 

220 
 _ > 

221 
assert false 

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

223  
224 
let get_type_definition tname = 

225 
type_coretype (fun _ > ()) (get_coretype_definition tname) 

226  
227 
(* Equality on ground types only *) 

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

229 
let rec eq_ground t1 t2 = 

230 
let t1 = repr t1 in 

231 
let t2 = repr t2 in 

232 
t1 == t2 

233 
 

234 
match t1.tdesc, t2.tdesc with 

235 
 Tbasic t1, Tbasic t2 when t1 == t2 > 

236 
true 

237 
 Tenum tl, Tenum tl' when tl == tl' > 

238 
true 

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

240 
List.for_all2 eq_ground tl tl' 

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

242 
List.for_all2 (fun (_, t) (_, t') > eq_ground t t') fl fl' 

243 
 Tconst t, _ > 

244 
let def_t = get_type_definition t in 

245 
eq_ground def_t t2 

246 
 _, Tconst t > 

247 
let def_t = get_type_definition t in 

248 
eq_ground t1 def_t 

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

250 
eq_ground t1 t1' && eq_ground t2 t2' 

251 
 Tclock t1', Tclock t2' > 

252 
eq_ground t1' t2' 

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

254 
> 

255 
Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2' 

256 
 _ > 

257 
false 

258  
259 
(** [unify t1 t2] unifies types [t1] and [t2] using standard destructive 

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

261 
is a expected/formal/spec type, [t2] is a computed/real/implem type, so in 

262 
case of unification error: expected type [t1], got type [t2]. If 

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

264 
unification is required, [t1] should furthermore be an instance of [t2] 

265 
and constants are handled differently.*) 

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

267 
let rec unif t1 t2 = 

178  268 
let t1 = repr t1 in 
179  269 
let t2 = repr t2 in 
180 
t1==t2  

270 
if t1 == t2 then () 

271 
else 

181  272 
match t1.tdesc, t2.tdesc with 
182 
 Tbasic t1, Tbasic t2 when t1 == t2 > true 

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

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

185 
 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' 

186 
 (Tconst t, _) > 

187 
let def_t = get_type_definition t in 

188 
eq_ground def_t t2 

189 
 (_, Tconst t) > 

190 
let def_t = get_type_definition t in 

191 
eq_ground t1 def_t 

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

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

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

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

196 
 _ > false 

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

199 
using standard destructive unification. 

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

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

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

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

204 
If [semi] unification is required, 

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

206 
and constants are handled differently.*) 

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

208 
let rec unif t1 t2 = 

209 
let t1 = repr t1 in 

210 
let t2 = repr t2 in 

211 
if t1 == t2 then 

273 
(* strictly subtyping cases first *) 

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

275 
unif t1 t2 

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

277 
unif t1 t2 

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

279 
 Tvar, Tvar > 

280 
if t1.tid < t2.tid then t2.tdesc < Tlink t1 else t1.tdesc < Tlink t2 

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

282 
t1.tdesc < Tlink t2 

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

284 
t2.tdesc < Tlink t1 

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

286 
unif t2 t2'; 

287 
unif t1' t1 

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

289 
List.iter2 unif tl tl' 

290 
 Ttuple [ t1 ], _ > 

291 
unif t1 t2 

292 
 _, Ttuple [ t2 ] > 

293 
unif t1 t2 

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

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

296 
 Tclock _, Tstatic _  Tstatic _, Tclock _ > 

297 
raise (Unify (t1, t2)) 

298 
 Tclock t1', Tclock t2' > 

299 
unif t1' t2' 

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

301 
 Tunivar, _  _, Tunivar > 

212  302 
() 
213 
else 

214 
match t1.tdesc,t2.tdesc with 

215 
(* strictly subtyping cases first *) 

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

217 
unif t1 t2 

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

219 
unif t1 t2 

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

221 
 Tvar, Tvar > 

222 
if t1.tid < t2.tid then 

223 
t2.tdesc < Tlink t1 

303 
 Tconst t, _ > 

304 
let def_t = get_type_definition t in 

305 
unif def_t t2 

306 
 _, Tconst t > 

307 
let def_t = get_type_definition t in 

308 
unif t1 def_t 

309 
 Tenum tl, Tenum tl' when tl == tl' > 

310 
() 

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

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

313 
let eval_const = 

314 
if semi then fun c > 

315 
Some (Dimension.mkdim_ident Location.dummy_loc c) 

316 
else fun _ > None 

317 
in 

318 
unif t1' t2'; 

319 
Dimension.eval Basic_library.eval_dim_env eval_const e1; 

320 
Dimension.eval Basic_library.eval_dim_env eval_const e2; 

321 
Dimension.unify ~semi e1 e2 

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

323 
for numerical constants with non static ones for variables with 

324 
possible machine types *) 

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

326 
BasicT.unify bt1 bt2 

327 
 _, _ > 

328 
raise (Unify (t1, t2)) 

329 
in 

330 
unif t1 t2 

331  
332 
(* Expected type ty1, got type ty2 *) 

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

334 
try unify ~sub ~semi ty1 ty2 with 

335 
 Unify (t1', t2') > 

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

337 
 Dimension.Unify _ > 

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

339  
340 
(************************************************) 

341 
(* Typing function for each basic AST construct *) 

342 
(************************************************) 

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

345 
if Hashtbl.mem field_table label then ( 

346 
let tydef = Hashtbl.find field_table label in 

347 
let tydec = (typedef_of_top tydef).tydef_desc in 

348 
let tydec_struct = get_struct_type_fields tydec in 

349 
let ty_label = 

350 
type_coretype (fun _ > ()) (List.assoc label tydec_struct) 

351 
in 

352 
try_unify ty_label (type_const ~is_annot loc c) loc; 

353 
type_coretype (fun _ > ()) tydec) 

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

355  
356 
and type_const ?(is_annot = false) loc c = 

357 
match c with 

358 
 Const_int _ > 

359 
(* Type_predef. *) 

360 
type_int 

361 
 Const_real _ > 

362 
(* Type_predef. *) 

363 
type_real 

364 
 Const_array ca > 

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

366 
let ty = new_var () in 

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

368 
(* Type_predef. *) 

369 
type_array d ty 

370 
 Const_tag t > 

371 
if Hashtbl.mem tag_table t then 

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

373 
let tydec = 

374 
if is_user_type tydef.tydef_desc then Tydec_const tydef.tydef_id 

375 
else tydef.tydef_desc 

376 
in 

377 
type_coretype (fun _ > ()) tydec 

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

379 
 Const_struct fl > ( 

380 
let ty_struct = new_var () in 

381 
let used = 

382 
List.fold_left 

383 
(fun acc (l, c) > 

384 
if List.mem l acc then 

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

224  386 
else 
225 
t1.tdesc < Tlink t2 

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

227 
t1.tdesc < Tlink t2 

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

229 
t2.tdesc < Tlink t1 

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

231 
begin 

232 
unif t2 t2'; 

233 
unif t1' t1 

234 
end 

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

236 
List.iter2 unif tl tl' 

237 
 Ttuple [t1] , _ > unif t1 t2 

238 
 _ , Ttuple [t2] > unif t1 t2 

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

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

241 
 Tclock _, Tstatic _ 

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

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

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

245 
 Tunivar, _  _, Tunivar > () 

246 
 (Tconst t, _) > 

247 
let def_t = get_type_definition t in 

248 
unif def_t t2 

249 
 (_, Tconst t) > 

250 
let def_t = get_type_definition t in 

251 
unif t1 def_t 

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

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

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

255 
let eval_const = 

256 
if semi 

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

258 
else (fun _ > None) in 

259 
begin 

260 
unif t1' t2'; 

261 
Dimension.eval Basic_library.eval_dim_env eval_const e1; 

262 
Dimension.eval Basic_library.eval_dim_env eval_const e2; 

263 
Dimension.unify ~semi:semi e1 e2; 

264 
end 

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

266 
for numerical constants with non static ones for variables with 

267 
possible machine types *) 

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

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

270 
in unif t1 t2 

271  
272 
(* Expected type ty1, got type ty2 *) 

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

387 
try_unify ty_struct 

388 
(type_struct_const_field ~is_annot loc (l, c)) 

389 
loc; 

390 
l :: acc) 

391 
[] fl 

392 
in 

274  393 
try 
275 
unify ~sub:sub ~semi:semi ty1 ty2 

276 
with 

277 
 Unify (t1', t2') > 

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

279 
 Dimension.Unify _ > 

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

281  
282  
283 
(************************************************) 

284 
(* Typing function for each basic AST construct *) 

285 
(************************************************) 

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

288 
if Hashtbl.mem field_table label 

289 
then let tydef = Hashtbl.find field_table label in 

290 
let tydec = (typedef_of_top tydef).tydef_desc in 

291 
let tydec_struct = get_struct_type_fields tydec in 

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

293 
begin 

294 
try_unify ty_label (type_const ~is_annot loc c) loc; 

295 
type_coretype (fun _ > ()) tydec 

296 
end 

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

298  
299 
and type_const ?(is_annot=false) loc c = 

300 
match c with 

301 
 Const_int _ > (* Type_predef. *)type_int 

302 
 Const_real _ > (* Type_predef. *)type_real 

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

304 
let ty = new_var () in 

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

306 
(* Type_predef. *)type_array d ty 

307 
 Const_tag t > 

308 
if Hashtbl.mem tag_table t 

309 
then 

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

311 
let tydec = 

312 
if is_user_type tydef.tydef_desc 

313 
then Tydec_const tydef.tydef_id 

314 
else tydef.tydef_desc in 

315 
type_coretype (fun _ > ()) tydec 

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

317 
 Const_struct fl > 

318 
let ty_struct = new_var () in 

319 
begin 

320 
let used = 

321 
List.fold_left 

322 
(fun acc (l, c) > 

323 
if List.mem l acc 

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

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

326 
[] fl in 

327 
try 

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

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

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

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

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

333 
with Not_found > 

334 
ty_struct 

335 
end 

336 
 Const_string s  Const_modeid s > 

337 
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 *)) 

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

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

341 
[env] is a pair composed of: 

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

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

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

345 
propagation policy in Lustre. 

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

347 
later discovered to be clocks during the typing process. 

348 
*) 

349 
let check_constant loc const_expected const_real = 

350 
if const_expected && not const_real 

351 
then raise (Error (loc, Not_a_constant)) 

352  
353 
let rec type_add_const env const arg targ = 

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

355 
if const 

356 
then let d = 

357 
if is_dimension_type targ 

358 
then dimension_of_expr arg 

359 
else Dimension.mkdim_var () in 

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

361 
Dimension.eval Basic_library.eval_dim_env eval_const d; 

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

363 
(match (* Types. *)get_static_value targ with 

364 
 None > () 

365 
 Some _ > try_unify targ real_static_type arg.expr_loc); 

366 
real_static_type 

367 
else targ 

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

370 
used during node applications and assignments *) 

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

372 
let loc = real_arg.expr_loc in 

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

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

375 
(*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;*) 

376 
try_unify ~sub:sub formal_type real_type loc 

377  
378 
(* typing an application implies: 

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

380 
 checking type adequation between formal and real arguments 

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

382 
it in many calls 

383 
*) 

384 
and type_appl env in_main loc const f args = 

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

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

387 
then 

388 
try 

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

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

391 
with 

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

393 


394 
let total = 

395 
List.map fst (get_struct_type_fields (coretype_type ty_struct)) 

396 
in 

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

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

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

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

401 
with Not_found > ty_struct) 

402 
 Const_string s  Const_modeid s > 

403 
if is_annot then (* Type_predef. *) 

404 
type_string 

394  405 
else ( 
395 
type_dependent_call env in_main loc const f (List.combine args targs) 

396 
) 

397 


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

399 
and type_dependent_call env in_main loc const f targs = 

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

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

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

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

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

405 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 

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

407 
let tins = type_list_of_type tins in 

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

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

410 
else 

411 
begin 

412 
List.iter2 ( 

413 
fun (a,t) ti > 

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

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

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

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

418 


419 
) 

420 
targs 

421 
tins; 

422 
touts 

423 
end 

424  
425 
(* type a simple call without dependent types 

426 
but possible homomorphic extension. 

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

428 
and type_simple_call env in_main loc const f targs = 

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

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

431 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 

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

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

434 
touts 

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

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

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

439 
let resulting_ty = 

440 
match expr.expr_desc with 

441 
 Expr_const c > 

442 
let ty = type_const ~is_annot expr.expr_loc c in 

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

444 
expr.expr_type < Expr_type_hub.export ty; 

445 
ty 

446 
 Expr_ident v > 

447 
let tyv = 

448 
try 

449 
Env.lookup_value (fst env) v 

450 
with Not_found > 

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

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

453 
in 

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

455 
let ty' = 

456 
if const 

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

458 
else new_var () in 

459 
try_unify ty ty' expr.expr_loc; 

460 
expr.expr_type < Expr_type_hub.export ty; 

461 
ty 

462 
 Expr_array elist > 

463 
let ty_elt = new_var () in 

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

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

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

467 
expr.expr_type < Expr_type_hub.export ty; 

468 
ty 

469 
 Expr_access (e1, d) > 

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

471 
let ty_elt = new_var () in 

472 
let d = Dimension.mkdim_var () in 

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

474 
expr.expr_type < Expr_type_hub.export ty_elt; 

475 
ty_elt 

476 
 Expr_power (e1, d) > 

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

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

479 
Dimension.eval Basic_library.eval_dim_env eval_const d; 

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

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

482 
expr.expr_type < Expr_type_hub.export ty; 

483 
ty 

484 
 Expr_tuple elist > 

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

486 
expr.expr_type < Expr_type_hub.export ty; 

487 
ty 

488 
 Expr_ite (c, t, e) > 

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

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

491 
expr.expr_type < Expr_type_hub.export ty; 

492 
ty 

493 
 Expr_appl (id, args, r) > 

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

495 
expression *) 

496 
(match r with 

497 
 None > () 

498 
 Some c > 

499 
check_constant expr.expr_loc const false; 

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

501 
let args_list = expr_list_of_expr args in 

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

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

504 
args.expr_type < Expr_type_hub.export targs; 

505 
expr.expr_type < Expr_type_hub.export touts; 

506 
touts 

507 
 Expr_fby (e1,e2) 

508 
 Expr_arrow (e1,e2) > 

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

510 
check_constant expr.expr_loc const false; 

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

512 
expr.expr_type < Expr_type_hub.export ty; 

513 
ty 

514 
 Expr_pre e > 

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

516 
check_constant expr.expr_loc const false; 

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

518 
expr.expr_type < Expr_type_hub.export ty; 

519 
ty 

520 
 Expr_when (e1,c,l) > 

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

522 
check_constant expr.expr_loc const false; 

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

524 
let expr_c = expr_of_ident c expr.expr_loc in 

525 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 

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

527 
expr.expr_type < Expr_type_hub.export ty; 

528 
ty 

529 
 Expr_merge (c,hl) > 

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

531 
check_constant expr.expr_loc const false; 

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

533 
let expr_c = expr_of_ident c expr.expr_loc in 

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

535 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 

536 
expr.expr_type < Expr_type_hub.export typ_out; 

537 
typ_out 

538 
in 

539 
Log.report ~level:3 (fun fmt > 

540 
Format.fprintf fmt "Type of expr %a: %a@ " 

541 
Printers.pp_expr expr (* Types. *)print_ty resulting_ty); 

542 
resulting_ty 

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

545 
let typ_in = new_var () in 

546 
let typ_out = new_var () in 

547 
try 

548 
let used_labels = 

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

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

551 
type_subtyping_arg env in_main const h typ_out; 

552 
if List.mem t accu 

553 
then raise (Error (loc, Already_bound t)) 

554 
else t :: accu) [] hl in 

555 
let type_labels = get_enum_type_tags (coretype_type typ_in) in 

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

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

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

559 
else (typ_in, typ_out) 

560 
with Unify (t1, t2) > 

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

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

564 
let type_eexpr env eexpr = 

565 
(type_expr 

566 
~is_annot:true 

567 
env 

568 
false (* not in main *) 

569 
false (* not a const *) 

570 
eexpr.eexpr_qfexpr) 

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

574 
let type_eq env in_main undefined_vars eq = 

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

576 
(* Check undefined variables, type lhs *) 

577 
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 

578 
let ty_lhs = type_expr env in_main false expr_lhs in 

579 
(* Check multiple variable definitions *) 

580 
let define_var id uvars = 

581 
if ISet.mem id uvars 

582 
then ISet.remove id uvars 

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

406 
Format.eprintf "Typing string %s outisde of annot scope@.@?" s; 

407 
assert false (* string datatype should only appear in annotations *)) 

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

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

411 
is a pair composed of:  a map from ident to type, associating to each 

412 
ident, i.e. variables, constants and (imported) nodes, its type including 

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

414 
constant propagation policy in Lustre.  a vdecl list, in order to modify 

415 
types of declared variables that are later discovered to be clocks during 

416 
the typing process. *) 

417 
let check_constant loc const_expected const_real = 

418 
if const_expected && not const_real then raise (Error (loc, Not_a_constant)) 

419  
420 
let rec type_add_const env const arg targ = 

421 
(*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg 

422 
Types.print_ty targ;*) 

423 
if const then ( 

424 
let d = 

425 
if is_dimension_type targ then dimension_of_expr arg 

426 
else Dimension.mkdim_var () 

427 
in 

428 
let eval_const id = 

429 
(* Types. *) 

430 
get_static_value (Env.lookup_value (fst env) id) 

431 
in 

432 
Dimension.eval Basic_library.eval_dim_env eval_const d; 

433 
let real_static_type = 

434 
(* Type_predef. *) 

435 
type_static d ((* Types. *) 

436 
dynamic_type targ) 

584  437 
in 
585 
(* check assignment of declared constant, assignment of clock *) 

586 
let ty_lhs = 

438 
(match (* Types. *) 

439 
get_static_value targ with 

440 
 None > 

441 
() 

442 
 Some _ > 

443 
try_unify targ real_static_type arg.expr_loc); 

444 
real_static_type) 

445 
else targ 

446  
447 
(* emulates a subtyping relation between types t and (d : t), used during node 

448 
applications and assignments *) 

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

450 
let loc = real_arg.expr_loc in 

451 
let const = 

452 
const 

453 
 (* Types. *) 

454 
get_static_value formal_type <> None 

455 
in 

456 
let real_type = 

457 
type_add_const env const real_arg (type_expr env in_main const real_arg) 

458 
in 

459 
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const 

460 
Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty 

461 
formal_type;*) 

462 
try_unify ~sub formal_type real_type loc 

463  
464 
(* typing an application implies:  checking that const formal parameters 

465 
match real const (maybe symbolic) arguments  checking type adequation 

466 
between formal and real arguments An application may embed an 

467 
homomorphic/internal function, in which case we need to split it in many 

468 
calls *) 

469 
and type_appl env in_main loc const f args = 

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

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

472 
then 

473 
try 

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

475 
(* Types. *) 

587  476 
type_of_type_list 
588 
(List.map2 (fun ty id > 

589 
if get_static_value ty <> None 

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

591 
match get_clock_base_type ty with 

592 
 None > ty 

593 
 Some ty > ty) 

594 
(type_list_of_type ty_lhs) eq.eq_lhs) in 

595 
let undefined_vars = 

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

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

598 
to a (always nonconstant) lhs variable *) 

599 
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; 

600 
undefined_vars 

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

604 
in environment [env] *) 

605 
let type_coreclock env ck id loc = 

606 
match ck.ck_dec_desc with 

607 
 Ckdec_any > () 

608 
 Ckdec_bool cl > 

609 
let dummy_id_expr = expr_of_ident id loc in 

610 
let when_expr = 

611 
List.fold_left 

612 
(fun expr (x, l) > 

613 
{expr_tag = new_tag (); 

614 
expr_desc= Expr_when (expr,x,l); 

615 
expr_type = Types.Main.new_var (); 

616 
expr_clock = Clocks.new_var true; 

617 
expr_delay = Delay.new_var (); 

618 
expr_loc=loc; 

619 
expr_annot = None}) 

620 
dummy_id_expr cl 

621 
in 

622 
ignore (type_expr env false false when_expr) 

623  
624 
let rec check_type_declaration loc cty = 

625 
match cty with 

626 
 Tydec_clock ty 

627 
 Tydec_array (_, ty) > check_type_declaration loc ty 

628 
 Tydec_const tname > 

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

630 
if not (Hashtbl.mem type_table cty) 

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

632 
 _ > () 

633  
634 
let type_var_decl vd_env env vdecl = 

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

636 
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; 

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

638 
let type_dim d = 

639 
begin 

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

641 
Dimension.eval Basic_library.eval_dim_env eval_const d; 

642 
end in 

643 
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in 

644  
645 
let ty_static = 

646 
if vdecl.var_dec_const 

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

648 
else ty in 

649 
(match vdecl.var_dec_value with 

650 
 None > () 

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

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

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

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

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

656 
new_env 

657  
658 
let type_var_decl_list vd_env env l = 

659 
List.fold_left (type_var_decl vd_env) env l 

660  
661 
let type_of_vlist vars = 

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

663 
type_of_type_list tyl 

664  
665 
let add_vdecl vd_env vdecl = 

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

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

668 
else vdecl::vd_env 

669  
670 
let check_vd_env vd_env = 

671 
ignore (List.fold_left add_vdecl [] vd_env) 

672  
673 
let type_contract env c = 

674 
let vd_env = c.consts @ c.locals in 

675 
check_vd_env vd_env; 

676 
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 

677 
(* typing stmts *) 

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

679 
let undefined_vars_init = 

477 
(List.map (type_simple_call env in_main loc const f) targs) 

478 
with Utils.TransposeError (l, l') > 

479 
raise (Error (loc, WrongMorphism (l, l'))) 

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

481  
482 
(* type a call with possible dependent types. [targs] is here a list of 

483 
(argument, type) pairs. *) 

484 
and type_dependent_call env in_main loc const f targs = 

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

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

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

488 
let tfun = 

489 
(* Type_predef. *) 

490 
type_arrow tins touts 

491 
in 

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

493 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 

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

495 
let tins = type_list_of_type tins in 

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

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

498 
else ( 

499 
List.iter2 

500 
(fun (a, t) ti > 

501 
let t' = 

502 
type_add_const env 

503 
(const 

504 
 (* Types. *) 

505 
get_static_value ti <> None) 

506 
a t 

507 
in 

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

509 
print_ty t' print_ty touts; *) 

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

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

512 
print_ty t' print_ty touts; *)) 

513 
targs tins; 

514 
touts) 

515  
516 
(* type a simple call without dependent types but possible homomorphic 

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

518 
and type_simple_call env in_main loc const f targs = 

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

520 
let tfun = 

521 
(* Type_predef. *) 

522 
type_arrow tins touts 

523 
in 

524 
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun; 

525 
(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty 

526 
(type_of_type_list targs);*) 

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

528 
touts 

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

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

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

533 
let resulting_ty = 

534 
match expr.expr_desc with 

535 
 Expr_const c > 

536 
let ty = type_const ~is_annot expr.expr_loc c in 

537 
let ty = 

538 
(* Type_predef. *) 

539 
type_static (Dimension.mkdim_var ()) ty 

540 
in 

541 
expr.expr_type < Expr_type_hub.export ty; 

542 
ty 

543 
 Expr_ident v > 

544 
let tyv = 

545 
try Env.lookup_value (fst env) v 

546 
with Not_found > 

547 
Format.eprintf 

548 
"Failure in typing expr %a. Not in typing environement@." 

549 
Printers.pp_expr expr; 

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

551 
in 

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

553 
let ty' = 

554 
if const then 

555 
(* Type_predef. *) 

556 
type_static (Dimension.mkdim_var ()) (new_var ()) 

557 
else new_var () 

558 
in 

559 
try_unify ty ty' expr.expr_loc; 

560 
expr.expr_type < Expr_type_hub.export ty; 

561 
ty 

562 
 Expr_array elist > 

563 
let ty_elt = new_var () in 

564 
List.iter 

565 
(fun e > 

566 
try_unify ty_elt 

567 
(type_appl env in_main expr.expr_loc const "uminus" [ e ]) 

568 
e.expr_loc) 

569 
elist; 

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

571 
let ty = 

572 
(* Type_predef. *) 

573 
type_array d ty_elt 

574 
in 

575 
expr.expr_type < Expr_type_hub.export ty; 

576 
ty 

577 
 Expr_access (e1, d) > 

578 
type_subtyping_arg env in_main false 

579 
(* not necessary a constant *) 

580 
(expr_of_dimension d) 

581 
(* Type_predef. *) 

582 
type_int; 

583 
let ty_elt = new_var () in 

584 
let d = Dimension.mkdim_var () in 

585 
type_subtyping_arg env in_main const e1 

586 
((* Type_predef. *) 

587 
type_array d ty_elt); 

588 
expr.expr_type < Expr_type_hub.export ty_elt; 

589 
ty_elt 

590 
 Expr_power (e1, d) > 

591 
let eval_const id = 

592 
(* Types. *) 

593 
get_static_value (Env.lookup_value (fst env) id) 

594 
in 

595 
type_subtyping_arg env in_main true (expr_of_dimension d) 

596 
(* Type_predef. *) 

597 
type_int; 

598 
Dimension.eval Basic_library.eval_dim_env eval_const d; 

599 
let ty_elt = 

600 
type_appl env in_main expr.expr_loc const "uminus" [ e1 ] 

601 
in 

602 
let ty = 

603 
(* Type_predef. *) 

604 
type_array d ty_elt 

605 
in 

606 
expr.expr_type < Expr_type_hub.export ty; 

607 
ty 

608 
 Expr_tuple elist > 

609 
let ty = 

610 
new_ty 

611 
(Ttuple (List.map (type_expr ~is_annot env in_main const) elist)) 

612 
in 

613 
expr.expr_type < Expr_type_hub.export ty; 

614 
ty 

615 
 Expr_ite (c, t, e) > 

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

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

618 
expr.expr_type < Expr_type_hub.export ty; 

619 
ty 

620 
 Expr_appl (id, args, r) > 

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

622 
expression *) 

623 
(match r with 

624 
 None > 

625 
() 

626 
 Some c > 

627 
check_constant expr.expr_loc const false; 

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

629 
let args_list = expr_list_of_expr args in 

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

631 
let targs = 

632 
new_ty 

633 
(Ttuple 

634 
(List.map (fun a > Expr_type_hub.import a.expr_type) args_list)) 

635 
in 

636 
args.expr_type < Expr_type_hub.export targs; 

637 
expr.expr_type < Expr_type_hub.export touts; 

638 
touts 

639 
 Expr_fby (e1, e2)  Expr_arrow (e1, e2) > 

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

641 
check_constant expr.expr_loc const false; 

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

643 
expr.expr_type < Expr_type_hub.export ty; 

644 
ty 

645 
 Expr_pre e > 

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

647 
check_constant expr.expr_loc const false; 

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

649 
expr.expr_type < Expr_type_hub.export ty; 

650 
ty 

651 
 Expr_when (e1, c, l) > 

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

653 
check_constant expr.expr_loc const false; 

654 
let typ_l = 

655 
(* Type_predef. *) 

656 
type_clock (type_const ~is_annot expr.expr_loc (Const_tag l)) 

657 
in 

658 
let expr_c = expr_of_ident c expr.expr_loc in 

659 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 

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

661 
expr.expr_type < Expr_type_hub.export ty; 

662 
ty 

663 
 Expr_merge (c, hl) > 

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

665 
check_constant expr.expr_loc const false; 

666 
let typ_in, typ_out = 

667 
type_branches env in_main expr.expr_loc const hl 

668 
in 

669 
let expr_c = expr_of_ident c expr.expr_loc in 

670 
let typ_l = 

671 
(* Type_predef. *) 

672 
type_clock typ_in 

673 
in 

674 
type_subtyping_arg env in_main ~sub:false const expr_c typ_l; 

675 
expr.expr_type < Expr_type_hub.export typ_out; 

676 
typ_out 

677 
in 

678 
Log.report ~level:3 (fun fmt > 

679 
Format.fprintf fmt "Type of expr %a: %a@ " Printers.pp_expr expr 

680 
(* Types. *) 

681 
print_ty resulting_ty); 

682 
resulting_ty 

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

685 
let typ_in = new_var () in 

686 
let typ_out = new_var () in 

687 
try 

688 
let used_labels = 

680  689 
List.fold_left 
681 
(fun uvs v > ISet.add v.var_id uvs) 

682 
ISet.empty c.locals 

690 
(fun accu (t, h) > 

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

692 
type_subtyping_arg env in_main const h typ_out; 

693 
if List.mem t accu then raise (Error (loc, Already_bound t)) 

694 
else t :: accu) 

695 
[] hl 

683  696 
in 
684 
let _ = 

697 
let type_labels = get_enum_type_tags (coretype_type typ_in) in 

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

699 
let unbound_tag = 

700 
List.find (fun t > not (List.mem t used_labels)) type_labels 

701 
in 

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

703 
else typ_in, typ_out 

704 
with Unify (t1, t2) > raise (Error (loc, Type_clash (t1, t2))) 

705  
706 
(* Eexpr are always in annotations. TODO: add the quantifiers variables to the 

707 
env *) 

708 
let type_eexpr env eexpr = 

709 
type_expr ~is_annot:true env false (* not in main *) false (* not a const *) 

710 
eexpr.eexpr_qfexpr 

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

713 
let type_eq env in_main undefined_vars eq = 

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

715 
(* Check undefined variables, type lhs *) 

716 
let expr_lhs = 

717 
expr_of_expr_list eq.eq_loc 

718 
(List.map (fun v > expr_of_ident v eq.eq_loc) eq.eq_lhs) 

719 
in 

720 
let ty_lhs = type_expr env in_main false expr_lhs in 

721 
(* Check multiple variable definitions *) 

722 
let define_var id uvars = 

723 
if ISet.mem id uvars then ISet.remove id uvars 

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

725 
in 

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

727 
let ty_lhs = 

728 
type_of_type_list 

729 
(List.map2 

730 
(fun ty id > 

731 
if get_static_value ty <> None then 

732 
raise (Error (eq.eq_loc, Assigned_constant id)) 

733 
else match get_clock_base_type ty with None > ty  Some ty > ty) 

734 
(type_list_of_type ty_lhs) eq.eq_lhs) 

735 
in 

736 
let undefined_vars = 

737 
List.fold_left 

738 
(fun uvars v > define_var v uvars) 

739 
undefined_vars eq.eq_lhs 

740 
in 

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

742 
assigned to a (always nonconstant) lhs variable *) 

743 
type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; 

744 
undefined_vars 

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

747 
environment [env] *) 

748 
let type_coreclock env ck id loc = 

749 
match ck.ck_dec_desc with 

750 
 Ckdec_any > 

751 
() 

752 
 Ckdec_bool cl > 

753 
let dummy_id_expr = expr_of_ident id loc in 

754 
let when_expr = 

685  755 
List.fold_left 
686 
(type_eq (env, vd_env) (false (*is_main*))) 

687 
undefined_vars_init 

688 
eqs 

689 
in 

690 
(* Typing each predicate expr *) 

691 
let type_pred_ee ee : unit= 

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

756 
(fun expr (x, l) > 

757 
{ 

758 
expr_tag = new_tag (); 

759 
expr_desc = Expr_when (expr, x, l); 

760 
expr_type = Types.Main.new_var (); 

761 
expr_clock = Clocks.new_var true; 

762 
expr_delay = Delay.new_var (); 

763 
expr_loc = loc; 

764 
expr_annot = None; 

765 
}) 

766 
dummy_id_expr cl 

693  767 
in 
694 
List.iter type_pred_ee 

695 
( 

696 
c.assume 

697 
@ c.guarantees 

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

699 
); 

700 
(*TODO 

701 
enrich env locally with locals and consts 

702 
type each pre/post as a boolean expr 

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

704 
For the moment, returning the provided env 

705 
*) 

768 
ignore (type_expr env false false when_expr) 

769  
770 
let rec check_type_declaration loc cty = 

771 
match cty with 

772 
 Tydec_clock ty  Tydec_array (_, ty) > 

773 
check_type_declaration loc ty 

774 
 Tydec_const tname > 

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

776 
if not (Hashtbl.mem type_table cty) then 

777 
raise (Error (loc, Unbound_type tname)) 

778 
 _ > 

779 
() 

780  
781 
let type_var_decl vd_env env vdecl = 

782 
(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl 

783 
Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*) 

784 
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc; 

785 
let eval_const id = 

786 
(* Types. *) 

787 
get_static_value (Env.lookup_value env id) 

788 
in 

789 
let type_dim d = 

790 
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) 

791 
(* Type_predef. *) 

792 
type_int; 

793 
Dimension.eval Basic_library.eval_dim_env eval_const d 

794 
in 

795 
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in 

796  
797 
let ty_static = 

798 
if vdecl.var_dec_const then 

799 
(* Type_predef. *) 

800 
type_static (Dimension.mkdim_var ()) ty 

801 
else ty 

802 
in 

803 
(match vdecl.var_dec_value with 

804 
 None > 

805 
() 

806 
 Some v > 

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

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

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

810 
type_coreclock (new_env, vd_env) vdecl.var_dec_clock vdecl.var_id 

811 
vdecl.var_loc; 

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

813 
new_env 

814  
815 
let type_var_decl_list vd_env env l = 

816 
List.fold_left (type_var_decl vd_env) env l 

817  
818 
let type_of_vlist vars = 

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

820 
type_of_type_list tyl 

821  
822 
let add_vdecl vd_env vdecl = 

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

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

825 
else vdecl :: vd_env 

826 
Also available in: Unified diff
reformatting