Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 7 months ago

reformatting

View differences:

src/checks/init_calculus.ml
12 12
(** Main typing module. Classic inference algorithm with destructive
13 13
    unification. *)
14 14

  
15
(* Though it shares similarities with the clock calculus module, no code
16
    is shared.  Simple environments, very limited identifier scoping, no
17
    identifier redefinition allowed. *)
15
(* Though it shares similarities with the clock calculus module, no code is
16
   shared. Simple environments, very limited identifier scoping, no identifier
17
   redefinition allowed. *)
18 18

  
19 19
open Utils
20
(* Yes, opening both modules is dirty as some type names will be
21
   overwritten, yet this makes notations far lighter.*)
20

  
21
(* Yes, opening both modules is dirty as some type names will be overwritten,
22
   yet this makes notations far lighter.*)
22 23
open Corelang
23 24
open Init
24 25
open Format
25 26

  
26
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in
27
    type [ty]. False otherwise. *)
27
(** [occurs tvar ty] returns true if the type variable [tvar] occurs in type
28
    [ty]. False otherwise. *)
28 29
let rec occurs tvar ty =
29 30
  let ty = repr ty in
30 31
  match ty.tdesc with
31
  | Ivar -> ty=tvar
32
  | Ivar ->
33
    ty = tvar
32 34
  | Iarrow (t1, t2) ->
33
      (occurs tvar t1) || (occurs tvar t2)
35
    occurs tvar t1 || occurs tvar t2
34 36
  | Ituple tl ->
35
      List.exists (occurs tvar) tl
36
  | Ilink t -> occurs tvar t
37
  | Isucc t -> occurs tvar t
38
  | Iunivar -> false
37
    List.exists (occurs tvar) tl
38
  | Ilink t ->
39
    occurs tvar t
40
  | Isucc t ->
41
    occurs tvar t
42
  | Iunivar ->
43
    false
39 44

  
40
(** Promote monomorphic type variables to polymorphic type variables. *)
41 45
(* Generalize by side-effects *)
46

  
47
(** Promote monomorphic type variables to polymorphic type variables. *)
42 48
let rec generalize ty =
43 49
  match ty.tdesc with
44 50
  | Ivar ->
45
      (* No scopes, always generalize *)
46
      ty.idesc <- Iunivar
47
  | Iarrow (t1,t2) ->
48
      generalize t1; generalize t2
51
    (* No scopes, always generalize *)
52
    ty.idesc <- Iunivar
53
  | Iarrow (t1, t2) ->
54
    generalize t1;
55
    generalize t2
49 56
  | Ituple tlist ->
50
      List.iter generalize tlist
57
    List.iter generalize tlist
51 58
  | Ilink t ->
52
      generalize t
59
    generalize t
53 60
  | Isucc t ->
54
      generalize t
55
  | Tunivar -> ()
61
    generalize t
62
  | Tunivar ->
63
    ()
56 64

  
57 65
(** Downgrade polymorphic type variables to monomorphic type variables *)
58 66
let rec instanciate inst_vars ty =
59 67
  let ty = repr ty in
60 68
  match ty.idesc with
61
  | Ivar -> ty
62
  | Iarrow (t1,t2) ->
63
      {ty with idesc =
64
       Iarrow ((instanciate inst_vars t1), (instanciate inst_vars t2))}
69
  | Ivar ->
70
    ty
71
  | Iarrow (t1, t2) ->
72
    {
73
      ty with
74
      idesc = Iarrow (instanciate inst_vars t1, instanciate inst_vars t2);
75
    }
65 76
  | Ituple tlist ->
66
      {ty with idesc = Ituple (List.map (instanciate inst_vars) tlist)}
77
    { ty with idesc = Ituple (List.map (instanciate inst_vars) tlist) }
67 78
  | Isucc t ->
68
	(* should not happen *)
69
	{ty with idesc = Isucc (instanciate inst_vars t)}
79
    (* should not happen *)
80
    { ty with idesc = Isucc (instanciate inst_vars t) }
70 81
  | Ilink t ->
71
	(* should not happen *)
72
	{ty with idesc = Ilink (instanciate inst_vars t)}
73
  | Iunivar ->
74
      try
75
        List.assoc ty.iid !inst_vars
76
      with Not_found ->
77
        let var = new_var () in
78
	inst_vars := (ty.iid, var)::!inst_vars;
79
	var
82
    (* should not happen *)
83
    { ty with idesc = Ilink (instanciate inst_vars t) }
84
  | Iunivar -> (
85
    try List.assoc ty.iid !inst_vars
86
    with Not_found ->
87
      let var = new_var () in
88
      inst_vars := (ty.iid, var) :: !inst_vars;
89
      var)
80 90

  
81
(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify
82
    (t1,t2)] if the types are not unifiable.*)
91
(** [unify env t1 t2] unifies types [t1] and [t2]. Raises [Unify (t1,t2)] if the
92
    types are not unifiable.*)
83 93

  
84 94
(* Standard destructive unification *)
85 95
(* may loop for omega types *)
86 96
let rec unify t1 t2 =
87 97
  let t1 = repr t1 in
88 98
  let t2 = repr t2 in
89
  if t1=t2 then
90
    ()
99
  if t1 = t2 then ()
91 100
  else
92 101
    (* No type abbreviations resolution for now *)
93
    match t1.idesc,t2.idesc with
94
      (* This case is not mandory but will keep "older" types *)
102
    match t1.idesc, t2.idesc with
103
    (* This case is not mandory but will keep "older" types *)
95 104
    | Ivar, Ivar ->
96
        if t1.iid < t2.iid then
97
          t2.idesc <- Ilink t1
98
        else
99
          t1.idesc <- Ilink t2
100
    | (Ivar, _) when (not (occurs t1 t2)) ->
101
        t1.idesc <- Ilink t2
102
    | (_,Ivar) when (not (occurs t2 t1)) ->
103
        t2.idesc <- Ilink t1
104
    | Isucc t1, Isucc t1' -> unify t1 t1'
105
    | Iarrow (t1,t2), Iarrow (t1',t2') ->
106
        unify t1 t1'; unify t2 t2'
105
      if t1.iid < t2.iid then t2.idesc <- Ilink t1 else t1.idesc <- Ilink t2
106
    | Ivar, _ when not (occurs t1 t2) ->
107
      t1.idesc <- Ilink t2
108
    | _, Ivar when not (occurs t2 t1) ->
109
      t2.idesc <- Ilink t1
110
    | Isucc t1, Isucc t1' ->
111
      unify t1 t1'
112
    | Iarrow (t1, t2), Iarrow (t1', t2') ->
113
      unify t1 t1';
114
      unify t2 t2'
107 115
    | Ituple tlist1, Ituple tlist2 ->
108
        if (List.length tlist1) <> (List.length tlist2) then
109
	  raise (Unify (t1, t2))
110
	else
111
          List.iter2 unify tlist1 tlist2
112
    | Iunivar,_ | _, Iunivar -> 
113
        ()
114
    | _,_ -> raise (Unify (t1, t2))
116
      if List.length tlist1 <> List.length tlist2 then raise (Unify (t1, t2))
117
      else List.iter2 unify tlist1 tlist2
118
    | Iunivar, _ | _, Iunivar ->
119
      ()
120
    | _, _ ->
121
      raise (Unify (t1, t2))
115 122

  
116
let init_of_const c = 
117
 Init_predef.init_zero
123
let init_of_const c = Init_predef.init_zero
118 124

  
119 125
let rec init_expect env in_main expr ty =
120 126
  let texpr = init_expr env in_main expr in
121
  try
122
    unify texpr ty
123
  with Unify (t1,t2) ->
124
    raise (Error (expr.expr_loc, Init_clash (t1,t2)))
127
  try unify texpr ty
128
  with Unify (t1, t2) -> raise (Error (expr.expr_loc, Init_clash (t1, t2)))
125 129

  
126
and init_ident env in_main id loc = 
127
  init_expr env in_main (expr_of_ident id loc)
130
and init_ident env in_main id loc = init_expr env in_main (expr_of_ident id loc)
128 131

  
129
(** [type_expr env in_main expr] types expression [expr] in environment
130
    [env]. *)
132
(** [type_expr env in_main expr] types expression [expr] in environment [env]. *)
131 133
and init_expr env in_main expr =
132 134
  match expr.expr_desc with
133 135
  | Expr_const c ->
134
      let ty = init_of_const c in
135
      expr.expr_init <- ty;
136
      ty
136
    let ty = init_of_const c in
137
    expr.expr_init <- ty;
138
    ty
137 139
  | Expr_ident v ->
138
      let tyv =
139
        try
140
          Env.lookup_value env v
141
        with Not_found ->
142
          raise (Error (expr.expr_loc, Unbound_value v))
143
      in
144
      let ty = instanciate (ref []) tyv in
145
      expr.expr_init <- ty;
146
      ty
140
    let tyv =
141
      try Env.lookup_value env v
142
      with Not_found -> raise (Error (expr.expr_loc, Unbound_value v))
143
    in
144
    let ty = instanciate (ref []) tyv in
145
    expr.expr_init <- ty;
146
    ty
147 147
  | Expr_tuple elist ->
148
      let ty = new_ty (Ttuple (List.map (type_expr env in_main) elist)) in
149
      expr.expr_init <- ty;
150
      ty
148
    let ty = new_ty (Ttuple (List.map (type_expr env in_main) elist)) in
149
    expr.expr_init <- ty;
150
    ty
151 151
  | Expr_appl (id, args, r) ->
152 152
    (match r with
153
    | None   -> ()
154
    | Some x -> let expr_x = expr_of_ident x expr.expr_loc in
155
		init_expect env in_main expr_x Init_predef.init_zero);
156
      let tfun = type_ident env in_main id expr.expr_loc in
157
      let tins,touts= split_arrow tfun in
158
      type_expect env in_main args tins;
159
      expr.expr_type <- touts;
160
      touts
161
  | Expr_arrow (e1,e2) ->
162
      let ty = type_expr env in_main e1 in
163
      type_expect env in_main e2 ty;
164
      expr.expr_type <- ty;
165
      ty
166
  | Expr_fby (init,e) ->
167
      let ty = type_of_const init in
168
      type_expect env in_main e ty;
169
      expr.expr_type <- ty;
170
      ty
171
  | Expr_concat (hd,e) ->
172
      let ty = type_of_const hd in
173
      type_expect env in_main e ty;
174
      expr.expr_type <- ty;
175
      ty
153
    | None ->
154
      ()
155
    | Some x ->
156
      let expr_x = expr_of_ident x expr.expr_loc in
157
      init_expect env in_main expr_x Init_predef.init_zero);
158
    let tfun = type_ident env in_main id expr.expr_loc in
159
    let tins, touts = split_arrow tfun in
160
    type_expect env in_main args tins;
161
    expr.expr_type <- touts;
162
    touts
163
  | Expr_arrow (e1, e2) ->
164
    let ty = type_expr env in_main e1 in
165
    type_expect env in_main e2 ty;
166
    expr.expr_type <- ty;
167
    ty
168
  | Expr_fby (init, e) ->
169
    let ty = type_of_const init in
170
    type_expect env in_main e ty;
171
    expr.expr_type <- ty;
172
    ty
173
  | Expr_concat (hd, e) ->
174
    let ty = type_of_const hd in
175
    type_expect env in_main e ty;
176
    expr.expr_type <- ty;
177
    ty
176 178
  | Expr_tail e ->
177
      let ty = type_expr env in_main e in
178
      expr.expr_type <- ty;
179
      ty
179
    let ty = type_expr env in_main e in
180
    expr.expr_type <- ty;
181
    ty
180 182
  | Expr_pre e ->
181
      let ty = type_expr env in_main e in
182
      expr.expr_type <- ty;
183
      ty
184
  | Expr_when (e1,c) | Expr_whennot (e1,c) ->
185
      let expr_c = expr_of_ident c expr.expr_loc in
186
      type_expect env in_main expr_c Type_predef.type_bool;
187
      let tlarg = type_expr env in_main e1 in
188
      expr.expr_type <- tlarg;
189
      tlarg
190
  | Expr_merge (c,e2,e3) ->
191
      let expr_c = expr_of_ident c expr.expr_loc in
192
      type_expect env in_main expr_c Type_predef.type_bool;
193
      let te2 = type_expr env in_main e2 in
194
      type_expect env in_main e3 te2;
195
      expr.expr_type <- te2;
196
      te2
197
  | Expr_uclock (e,k) | Expr_dclock (e,k) ->
198
      let ty = type_expr env in_main e in
199
      expr.expr_type <- ty;
200
      ty
201
  | Expr_phclock (e,q) ->
202
      let ty = type_expr env in_main e in
203
      expr.expr_type <- ty;
204
      ty
183
    let ty = type_expr env in_main e in
184
    expr.expr_type <- ty;
185
    ty
186
  | Expr_when (e1, c) | Expr_whennot (e1, c) ->
187
    let expr_c = expr_of_ident c expr.expr_loc in
188
    type_expect env in_main expr_c Type_predef.type_bool;
189
    let tlarg = type_expr env in_main e1 in
190
    expr.expr_type <- tlarg;
191
    tlarg
192
  | Expr_merge (c, e2, e3) ->
193
    let expr_c = expr_of_ident c expr.expr_loc in
194
    type_expect env in_main expr_c Type_predef.type_bool;
195
    let te2 = type_expr env in_main e2 in
196
    type_expect env in_main e3 te2;
197
    expr.expr_type <- te2;
198
    te2
199
  | Expr_uclock (e, k) | Expr_dclock (e, k) ->
200
    let ty = type_expr env in_main e in
201
    expr.expr_type <- ty;
202
    ty
203
  | Expr_phclock (e, q) ->
204
    let ty = type_expr env in_main e in
205
    expr.expr_type <- ty;
206
    ty
205 207

  
206 208
(** [type_eq env eq] types equation [eq] in environment [env] *)
207 209
let type_eq env in_main undefined_vars eq =
208 210
  (* Check multiple variable definitions *)
209 211
  let define_var id uvars =
210 212
    try
211
      ignore(IMap.find id uvars);
213
      ignore (IMap.find id uvars);
212 214
      IMap.remove id uvars
213
    with Not_found ->
214
      raise (Error (eq.eq_loc, Already_defined id))
215
    with Not_found -> raise (Error (eq.eq_loc, Already_defined id))
215 216
  in
216 217
  let undefined_vars =
217
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
218
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs
219
  in
218 220
  (* Type lhs *)
219 221
  let get_value_type id =
220
    try
221
      Env.lookup_value env id
222
    with Not_found ->
223
      raise (Error (eq.eq_loc, Unbound_value id))
222
    try Env.lookup_value env id
223
    with Not_found -> raise (Error (eq.eq_loc, Unbound_value id))
224 224
  in
225 225
  let tyl_lhs = List.map get_value_type eq.eq_lhs in
226 226
  let ty_lhs = type_of_type_list tyl_lhs in
227
  (* Type rhs *) 
227
  (* Type rhs *)
228 228
  type_expect env in_main eq.eq_rhs ty_lhs;
229 229
  undefined_vars
230 230

  
231 231
(* [type_coretype cty] types the type declaration [cty] *)
232 232
let type_coretype cty =
233 233
  match cty with
234
  | Tydec_any -> new_var ()
235
  | Tydec_int -> Type_predef.type_int
236
  | Tydec_real -> Type_predef.type_real
237
  | Tydec_float -> Type_predef.type_real
238
  | Tydec_bool -> Type_predef.type_bool
239
  | Tydec_clock -> Type_predef.type_clock
234
  | Tydec_any ->
235
    new_var ()
236
  | Tydec_int ->
237
    Type_predef.type_int
238
  | Tydec_real ->
239
    Type_predef.type_real
240
  | Tydec_float ->
241
    Type_predef.type_real
242
  | Tydec_bool ->
243
    Type_predef.type_bool
244
  | Tydec_clock ->
245
    Type_predef.type_clock
240 246

  
241
(* [type_coreclock env ck id loc] types the type clock declaration [ck]
242
   in environment [env] *)
247
(* [type_coreclock env ck id loc] types the type clock declaration [ck] in
248
   environment [env] *)
243 249
let type_coreclock env ck id loc =
244 250
  match ck.ck_dec_desc with
245
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
251
  | Ckdec_any | Ckdec_pclock (_, _) ->
252
    ()
246 253
  | Ckdec_bool cl ->
247
      let dummy_id_expr = expr_of_ident id loc in
248
      let when_expr =
249
        List.fold_left
250
          (fun expr c ->
251
            match c with
252
            | Wtrue id ->
253
                {expr_tag = new_tag ();
254
                 expr_desc=Expr_when (expr,id);
255
                 expr_type = new_var ();
256
                 expr_clock = Clocks.new_var true;
257
                 expr_loc=loc}
258
            | Wfalse id ->
259
                {expr_tag = new_tag ();
260
                 expr_desc=Expr_whennot (expr,id);
261
                 expr_type = new_var ();
262
                 expr_clock = Clocks.new_var true;
263
                 expr_loc=loc})
264
          dummy_id_expr cl
265
      in
266
      ignore (type_expr env false when_expr)
254
    let dummy_id_expr = expr_of_ident id loc in
255
    let when_expr =
256
      List.fold_left
257
        (fun expr c ->
258
          match c with
259
          | Wtrue id ->
260
            {
261
              expr_tag = new_tag ();
262
              expr_desc = Expr_when (expr, id);
263
              expr_type = new_var ();
264
              expr_clock = Clocks.new_var true;
265
              expr_loc = loc;
266
            }
267
          | Wfalse id ->
268
            {
269
              expr_tag = new_tag ();
270
              expr_desc = Expr_whennot (expr, id);
271
              expr_type = new_var ();
272
              expr_clock = Clocks.new_var true;
273
              expr_loc = loc;
274
            })
275
        dummy_id_expr cl
276
    in
277
    ignore (type_expr env false when_expr)
267 278

  
268 279
let type_var_decl env vdecl =
269
  if (Env.exists_value env vdecl.var_id) then
270
    raise (Error (vdecl.var_loc,Already_bound vdecl.var_id))
280
  if Env.exists_value env vdecl.var_id then
281
    raise (Error (vdecl.var_loc, Already_bound vdecl.var_id))
271 282
  else
272 283
    let ty = type_coretype vdecl.var_dec_type.ty_dec_desc in
273 284
    let new_env = Env.add_value env vdecl.var_id ty in
......
275 286
    vdecl.var_type <- ty;
276 287
    new_env
277 288

  
278
let type_var_decl_list env l =
279
  List.fold_left type_var_decl env l
289
let type_var_decl_list env l = List.fold_left type_var_decl env l
280 290

  
281 291
let type_of_vlist vars =
282 292
  let tyl = List.map (fun v -> v.var_type) vars in
283 293
  type_of_type_list tyl
284
      
285
(** [type_node env nd loc] types node [nd] in environment env. The
286
    location is used for error reports. *)
294

  
295
(** [type_node env nd loc] types node [nd] in environment env. The location is
296
    used for error reports. *)
287 297
let type_node env nd loc =
288 298
  let is_main = nd.node_id = !Options.main_node in
289 299
  let delta_env = type_var_decl_list IMap.empty nd.node_inputs in
......
293 303
  let undefined_vars_init =
294 304
    List.fold_left
295 305
      (fun uvs v -> IMap.add v.var_id () uvs)
296
      IMap.empty (nd.node_outputs@nd.node_locals) in
306
      IMap.empty
307
      (nd.node_outputs @ nd.node_locals)
308
  in
297 309
  let undefined_vars =
298 310
    List.fold_left (type_eq new_env is_main) undefined_vars_init nd.node_eqs
299 311
  in
300 312
  (* check that table is empty *)
301
  if (not (IMap.is_empty undefined_vars)) then
302
    raise (Error (loc,Undefined_var undefined_vars));
313
  if not (IMap.is_empty undefined_vars) then
314
    raise (Error (loc, Undefined_var undefined_vars));
303 315
  let ty_ins = type_of_vlist nd.node_inputs in
304 316
  let ty_outs = type_of_vlist nd.node_outputs in
305
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
317
  let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in
306 318
  generalize ty_node;
307 319
  (* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
308 320
  nd.node_type <- ty_node;
......
310 322

  
311 323
let type_imported_node env nd loc =
312 324
  let new_env = type_var_decl_list env nd.nodei_inputs in
313
  ignore(type_var_decl_list new_env nd.nodei_outputs);
325
  ignore (type_var_decl_list new_env nd.nodei_outputs);
314 326
  let ty_ins = type_of_vlist nd.nodei_inputs in
315 327
  let ty_outs = type_of_vlist nd.nodei_outputs in
316
  let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
328
  let ty_node = new_ty (Tarrow (ty_ins, ty_outs)) in
317 329
  generalize ty_node;
318
  if (is_polymorphic ty_node) then
330
  if is_polymorphic ty_node then
319 331
    raise (Error (loc, Poly_imported_node nd.nodei_id));
320 332
  let new_env = Env.add_value env nd.nodei_id ty_node in
321 333
  nd.nodei_type <- ty_node;
......
323 335

  
324 336
let type_top_decl env decl =
325 337
  match decl.top_decl_desc with
326
  | Node nd -> 
327
      type_node env nd decl.top_decl_loc
338
  | Node nd ->
339
    type_node env nd decl.top_decl_loc
328 340
  | ImportedNode nd ->
329
      type_imported_node env nd decl.top_decl_loc
330
  | SensorDecl _ | ActuatorDecl _ | Consts _ -> env
341
    type_imported_node env nd decl.top_decl_loc
342
  | SensorDecl _ | ActuatorDecl _ | Consts _ ->
343
    env
331 344

  
332 345
let type_top_consts env decl =
333 346
  match decl.top_decl_desc with
334
    | Consts clist -> 
335
      List.fold_left (fun env (id, c) ->
336
	let ty = type_of_const c in
337
	Env.add_value env id ty       
338
      ) env clist
339
    | Node _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ -> env
347
  | Consts clist ->
348
    List.fold_left
349
      (fun env (id, c) ->
350
        let ty = type_of_const c in
351
        Env.add_value env id ty)
352
      env clist
353
  | Node _ | ImportedNode _ | SensorDecl _ | ActuatorDecl _ ->
354
    env
340 355

  
341 356
let type_prog env decls =
342 357
  let new_env = List.fold_left type_top_consts env decls in
343
  ignore(List.fold_left type_top_decl new_env decls)
358
  ignore (List.fold_left type_top_decl new_env decls)
344 359

  
345 360
(* Local Variables: *)
346 361
(* compile-command:"make -C .." *)

Also available in: Unified diff