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 side-effects *) |
|
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 side-effects *) |
|
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 non-constant) 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 non-constant) 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