## lustrec / src / typing.ml @ e8250987

History | View | Annotate | Download (38.2 KB)

1 | a2d97a3e | ploc | (********************************************************************) |
---|---|---|---|

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 | 22fe1c93 | ploc | |

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 | 8446bf03 | ploc | open Lustre_types |

26 | 22fe1c93 | ploc | open Corelang |

27 | open Format |
||

28 | |||

29 | 66359a5e | ploc | |

30 | 217837e2 | ploc | (* TODO general remark: expect in the add_vdelc, 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 | 66359a5e | ploc | 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 | 34d3f022 | ploc | struct |

45 | 66359a5e | ploc | |

46 | 34d3f022 | ploc | module TP = Type_predef.Make (T) |

47 | include TP |
||

48 | 66359a5e | ploc | |

49 | 34d3f022 | ploc | 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 side-effects *) |
||

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 | 22fe1c93 | ploc | try |

167 | 34d3f022 | ploc | 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 | 6afa892a | xthirioux | 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 | 34d3f022 | ploc | 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 | 22fe1c93 | ploc | else |

215 | 34d3f022 | ploc | 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 | 66359a5e | ploc | for numerical constants with non static ones for variables with |

268 | possible machine types *) |
||

269 | 34d3f022 | ploc | | 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 | 21485807 | xthirioux | try |

276 | 34d3f022 | ploc | 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 | 21485807 | xthirioux | List.iter (fun l -> Format.eprintf "used: %s@." l) used; *) |

332 | 34d3f022 | ploc | let undef = List.find (fun l -> not (List.mem l used)) total |

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

334 | with Not_found -> |
||

335 | ty_struct |
||

336 | end |
||

337 | | Const_string _ | Const_modeid _ -> |
||

338 | if is_annot then (* Type_predef. *)type_string else assert false (* string datatype should only appear in annotations *) |
||

339 | |||

340 | (* The following typing functions take as parameter an environment [env] |
||

341 | 22fe1c93 | ploc | 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 | 34d3f022 | ploc | *) |

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 | 4a840259 | xthirioux | used during node applications and assignments *) |

372 | 34d3f022 | ploc | 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 | 22fe1c93 | ploc | - checking that const formal parameters match real const (maybe symbolic) arguments |

381 | - checking type adequation between formal and real arguments |
||

382 | b616fe7a | xthirioux | An application may embed an homomorphic/internal function, in which case we need to split |

383 | it in many calls |
||

384 | 34d3f022 | ploc | *) |

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 | 66359a5e | ploc | ) |

398 | 307c32f5 | ploc | |

399 | 34d3f022 | ploc | (* 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 | a38c681e | xthirioux | but possible homomorphic extension. |

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

429 | 34d3f022 | ploc | 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 | 22fe1c93 | ploc | [env], expecting it to be [const] or not. *) |

439 | 34d3f022 | ploc | 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 | 5c1184ad | ploc | expression *) |

497 | 34d3f022 | ploc | (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 | 307c32f5 | ploc | let touts = type_appl env in_main expr.expr_loc const id args_list in |

504 | 34d3f022 | ploc | 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 | 22fe1c93 | ploc | to a (always non-constant) lhs variable *) |

598 | 34d3f022 | ploc | type_subtyping_arg env in_main false eq.eq_rhs ty_lhs; |

599 | undefined_vars |
||

600 | 22fe1c93 | ploc | |

601 | |||

602 | 34d3f022 | ploc | (* [type_coreclock env ck id loc] types the type clock declaration [ck] |

603 | 22fe1c93 | ploc | in environment [env] *) |

604 | 34d3f022 | ploc | 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 | 217837e2 | ploc | let type_spec env spec = |

673 | let vd_env = spec.consts @ spec.locals in |
||

674 | check_vd_env vd_env; |
||

675 | let env = type_var_decl_list ((* this argument seems useless to me, cf TODO at top of the file*) vd_env) env vd_env in |
||

676 | (* typing stmts *) |
||

677 | let eqs = List.map (fun s -> match s with Eq eq -> eq | _ -> assert false) spec.stmts in |
||

678 | let undefined_vars_init = |
||

679 | List.fold_left |
||

680 | (fun uvs v -> ISet.add v.var_id uvs) |
||

681 | ISet.empty spec.locals |
||

682 | in |
||

683 | let _ = |
||

684 | List.fold_left |
||

685 | (type_eq (env, vd_env) (false (*is_main*))) |
||

686 | undefined_vars_init |
||

687 | eqs |
||

688 | in |
||

689 | |||

690 | 34d3f022 | ploc | (*TODO |

691 | enrich env locally with locals and consts |
||

692 | type each pre/post as a boolean expr |
||

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

694 | For the moment, returning the provided env |
||

695 | *) |
||

696 | env |
||

697 | |||

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

699 | location is used for error reports. *) |
||

700 | let type_node env nd loc = |
||

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

702 | let vd_env_ol = nd.node_outputs@nd.node_locals in |
||

703 | let vd_env = nd.node_inputs@vd_env_ol in |
||

704 | check_vd_env vd_env; |
||

705 | let init_env = env in |
||

706 | let delta_env = type_var_decl_list vd_env init_env nd.node_inputs in |
||

707 | let delta_env = type_var_decl_list vd_env delta_env nd.node_outputs in |
||

708 | let delta_env = type_var_decl_list vd_env delta_env nd.node_locals in |
||

709 | let new_env = Env.overwrite env delta_env in |
||

710 | let undefined_vars_init = |
||

711 | 22fe1c93 | ploc | List.fold_left |

712 | 34d3f022 | ploc | (fun uvs v -> ISet.add v.var_id uvs) |

713 | ISet.empty vd_env_ol in |
||

714 | let undefined_vars = |
||

715 | let eqs, auts = get_node_eqs nd in |
||

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

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

718 | 22fe1c93 | ploc | in |

719 | 34d3f022 | ploc | (* Typing asserts *) |

720 | List.iter (fun assert_ -> |
||

721 | let assert_expr = assert_.assert_expr in |
||

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

723 | ) nd.node_asserts; |
||

724 | (* Typing spec/contracts *) |
||

725 | 217837e2 | ploc | (match nd.node_spec with None -> () | Some spec -> ignore (type_spec new_env spec)); |

726 | 34d3f022 | ploc | (* Typing annots *) |

727 | List.iter (fun annot -> |
||

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

729 | ) nd.node_annot; |
||

730 | |||

731 | (* check that table is empty *) |
||

732 | 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 |
||

733 | let undefined_vars = ISet.diff undefined_vars local_consts in |
||

734 | if (not (ISet.is_empty undefined_vars)) then |
||

735 | raise (Error (loc, Undefined_var undefined_vars)); |
||

736 | let ty_ins = type_of_vlist nd.node_inputs in |
||

737 | let ty_outs = type_of_vlist nd.node_outputs in |
||

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

739 | generalize ty_node; |
||

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

741 | nd.node_type <- Expr_type_hub.export ty_node; |
||

742 | Env.add_value env nd.node_id ty_node |
||

743 | |||

744 | let type_imported_node env nd loc = |
||

745 | let vd_env = nd.nodei_inputs@nd.nodei_outputs in |
||

746 | check_vd_env vd_env; |
||

747 | 217837e2 | ploc | let delta_env = type_var_decl_list vd_env env nd.nodei_inputs in |

748 | let delta_env = type_var_decl_list vd_env delta_env nd.nodei_outputs in |
||

749 | let new_env = Env.overwrite env delta_env in |
||

750 | (* Typing spec *) |
||

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

752 | 34d3f022 | ploc | let ty_ins = type_of_vlist nd.nodei_inputs in |

753 | let ty_outs = type_of_vlist nd.nodei_outputs in |
||

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

755 | generalize ty_node; |
||

756 | (* |
||

757 | 22fe1c93 | ploc | if (is_polymorphic ty_node) then |

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

759 | 34d3f022 | ploc | *) |

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

761 | nd.nodei_type <- Expr_type_hub.export ty_node; |
||

762 | new_env |
||

763 | |||

764 | let type_top_const env cdecl = |
||

765 | let ty = type_const cdecl.const_loc cdecl.const_value in |
||

766 | let d = |
||

767 | if is_dimension_type ty |
||

768 | then dimension_of_const cdecl.const_loc cdecl.const_value |
||

769 | else Dimension.mkdim_var () in |
||

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

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

772 | cdecl.const_type <- Expr_type_hub.export ty; |
||

773 | new_env |
||

774 | |||

775 | let type_top_consts env clist = |
||

776 | List.fold_left type_top_const env clist |
||

777 | |||

778 | let rec type_top_decl env decl = |
||

779 | match decl.top_decl_desc with |
||

780 | | Node nd -> ( |
||

781 | try |
||

782 | type_node env nd decl.top_decl_loc |
||

783 | with Error (loc, err) as exc -> ( |
||

784 | if !Options.global_inline then |
||

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

786 | Printers.pp_node nd |
||

787 | ; |
||

788 | raise exc) |
||

789 | ) |
||

790 | | ImportedNode nd -> |
||

791 | type_imported_node env nd decl.top_decl_loc |
||

792 | | Const c -> |
||

793 | type_top_const env c |
||

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

795 | 19a1e66b | ploc | | Include _ | Open _ -> env |

796 | 0d54d8a8 | ploc | |

797 | 34d3f022 | ploc | let get_type_of_call decl = |

798 | match decl.top_decl_desc with |
||

799 | | Node nd -> |
||

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

801 | type_list_of_type in_typ, type_list_of_type out_typ |
||

802 | | ImportedNode nd -> |
||

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

804 | type_list_of_type in_typ, type_list_of_type out_typ |
||

805 | | _ -> assert false |
||

806 | |||

807 | let type_prog env decls = |
||

808 | try |
||

809 | List.fold_left type_top_decl env decls |
||

810 | with Failure _ as exc -> raise exc |
||

811 | |||

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

813 | original description of dimensions, with constant parameters, |
||

814 | instead of unifiable internal variables. *) |
||

815 | |||

816 | (* The following functions aims at 'unevaluating' dimension |
||

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

818 | second_order variables with the original static parameters. |
||

819 | Once restored in this formulation, dimensions may be |
||

820 | meaningfully printed. *) |
||

821 | let uneval_vdecl_generics vdecl = |
||

822 | if vdecl.var_dec_const |
||

823 | then |
||

824 | match get_static_value (Expr_type_hub.import vdecl.var_type) with |
||

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

826 | | Some d -> Dimension.uneval vdecl.var_id d |
||

827 | |||

828 | let uneval_node_generics vdecls = |
||

829 | List.iter uneval_vdecl_generics vdecls |
||

830 | |||

831 | let uneval_spec_generics spec = |
||

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

833 | |||

834 | let uneval_top_generics decl = |
||

835 | match decl.top_decl_desc with |
||

836 | | Node nd -> |
||

837 | uneval_node_generics (nd.node_inputs @ nd.node_outputs) |
||

838 | | ImportedNode nd -> |
||

839 | uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs) |
||

840 | 19a1e66b | ploc | | Const _ | TypeDef _ | Open _ | Include _ |

841 | 34d3f022 | ploc | -> () |

842 | |||

843 | let uneval_prog_generics prog = |
||

844 | List.iter uneval_top_generics prog |
||

845 | |||

846 | let rec get_imported_symbol decls id = |
||

847 | match decls with |
||

848 | | [] -> assert false |
||

849 | | decl::q -> |
||

850 | (match decl.top_decl_desc with |
||

851 | | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl |
||

852 | | Const c when id = c.const_id && decl.top_decl_itf -> decl |
||

853 | | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id |
||

854 | | _ -> get_imported_symbol q id) |
||

855 | |||

856 | let check_env_compat header declared computed = |
||

857 | uneval_prog_generics header; |
||

858 | Env.iter declared (fun k decl_type_k -> |
||

859 | let loc = (get_imported_symbol header k).top_decl_loc in |
||

860 | let computed_t = |
||

861 | instantiate (ref []) (ref []) |
||

862 | (try Env.lookup_value computed k |
||

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

864 | (*Types.print_ty Format.std_formatter decl_type_k; |
||

865 | ef34b4ae | xthirioux | Types.print_ty Format.std_formatter computed_t;*) |

866 | 34d3f022 | ploc | try_unify ~sub:true ~semi:true decl_type_k computed_t loc |

867 | ) |
||

868 | |||

869 | let check_typedef_top decl = |
||

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

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

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

873 | match decl.top_decl_desc with |
||

874 | | TypeDef ty -> |
||

875 | let owner = decl.top_decl_owner in |
||

876 | let itf = decl.top_decl_itf in |
||

877 | let decl' = |
||

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

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

880 | let owner' = decl'.top_decl_owner in |
||

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

882 | let itf' = decl'.top_decl_itf in |
||

883 | (match decl'.top_decl_desc with |
||

884 | | Const _ | Node _ | ImportedNode _ -> assert false |
||

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

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

887 | | _ -> () |
||

888 | |||

889 | let check_typedef_compat header = |
||

890 | List.iter check_typedef_top header |
||

891 | end |
||

892 | 5c1184ad | ploc | |

893 | 66359a5e | ploc | include Make(Types.Main) (struct |

894 | 34d3f022 | ploc | type type_expr = Types.Main.type_expr |

895 | let import x = x |
||

896 | let export x = x |
||

897 | end) |
||

898 | (* Local Variables: *) |
||

899 | (* compile-command:"make -C .." *) |
||

900 | 22fe1c93 | ploc | (* End: *) |