Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ 5fccce23

History | View | Annotate | Download (26.7 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
14 22fe1c93 ploc
15
(** Main clock-calculus module. Based on type inference algorithms with
16
  destructive unification. Uses a bit of subtyping for periodic clocks. *)
17
18
(* Though it shares similarities with the typing module, no code
19
    is shared.  Simple environments, very limited identifier scoping, no
20
    identifier redefinition allowed. *)
21
open Utils
22 8446bf03 ploc
open Lustre_types
23 22fe1c93 ploc
open Corelang
24
open Clocks
25
open Format
26
27
let loc_of_cond loc_containing id =
28
  let pos_start =
29
    {loc_containing.Location.loc_end with 
30
     Lexing.pos_cnum=loc_containing.Location.loc_end.Lexing.pos_cnum-(String.length id)}
31
  in
32
  {Location.loc_start = pos_start;
33
   Location.loc_end = loc_containing.Location.loc_end}
34
35
(** [occurs cvar ck] returns true if the clock variable [cvar] occurs in
36
    clock [ck]. False otherwise. *)
37
let rec occurs cvar ck =
38
  let ck = repr ck in
39
  match ck.cdesc with
40
  | Carrow (ck1, ck2) ->
41
      (occurs cvar ck1) || (occurs cvar ck2)
42
  | Ctuple ckl ->
43
      List.exists (occurs cvar) ckl
44
  | Con (ck',_,_) -> occurs cvar ck'
45 45f0f48d xthirioux
  | Cvar  -> ck=cvar
46
  | Cunivar   -> false
47 22fe1c93 ploc
  | Clink ck' -> occurs cvar ck'
48
  | Ccarrying (_,ck') -> occurs cvar ck'
49
50
(* Clocks generalization *)
51
let rec generalize_carrier cr =
52
  match cr.carrier_desc with
53
  | Carry_const _
54
  | Carry_name ->
55
      if cr.carrier_scoped then
56
        raise (Scope_carrier cr);
57
      cr.carrier_desc <- Carry_var
58
  | Carry_var -> ()
59
  | Carry_link cr' -> generalize_carrier cr'
60
61
(** Promote monomorphic clock variables to polymorphic clock variables. *)
62
(* Generalize by side-effects *)
63
let rec generalize ck =
64
    match ck.cdesc with
65
    | Carrow (ck1,ck2) ->
66
        generalize ck1; generalize ck2
67
    | Ctuple clist ->
68
        List.iter generalize clist
69
    | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
70 45f0f48d xthirioux
    | Cvar ->
71 22fe1c93 ploc
        if ck.cscoped then
72
          raise (Scope_clock ck);
73 45f0f48d xthirioux
        ck.cdesc <- Cunivar 
74
    | Cunivar -> () 
75 22fe1c93 ploc
    | Clink ck' ->
76
        generalize ck'
77
    | Ccarrying (cr,ck') ->
78
        generalize_carrier cr; generalize ck'
79
80
let try_generalize ck_node loc =
81
  try 
82
    generalize ck_node
83
  with (Scope_carrier cr) ->
84
    raise (Error (loc, Carrier_extrusion (ck_node, cr)))
85
  | (Scope_clock ck) ->
86
    raise (Error (loc, Clock_extrusion (ck_node, ck)))
87
88
(* Clocks instanciation *)
89 7291cb80 xthirioux
let instantiate_carrier cr inst_cr_vars =
90 22fe1c93 ploc
  let cr = carrier_repr cr in
91
  match cr.carrier_desc with
92
  | Carry_const _
93
  | Carry_name -> cr
94
  | Carry_link _ ->
95
      failwith "Internal error"
96
  | Carry_var ->
97
      try
98
        List.assoc cr.carrier_id !inst_cr_vars
99
      with Not_found ->            
100
        let cr_var = new_carrier Carry_name true in
101
        inst_cr_vars := (cr.carrier_id,cr_var)::!inst_cr_vars;
102
        cr_var
103
104
(** Downgrade polymorphic clock variables to monomorphic clock variables *)
105
(* inst_ck_vars ensures that a polymorphic variable is instanciated with
106
   the same monomorphic variable if it occurs several times in the same
107
   type. inst_cr_vars is the same for carriers. *)
108 7291cb80 xthirioux
let rec instantiate inst_ck_vars inst_cr_vars ck =
109 22fe1c93 ploc
  match ck.cdesc with
110
  | Carrow (ck1,ck2) ->
111
      {ck with cdesc =
112 7291cb80 xthirioux
       Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),
113
               (instantiate inst_ck_vars inst_cr_vars ck2))}
114 22fe1c93 ploc
  | Ctuple cklist ->
115
      {ck with cdesc = Ctuple 
116 7291cb80 xthirioux
         (List.map (instantiate inst_ck_vars inst_cr_vars) cklist)}
117 22fe1c93 ploc
  | Con (ck',c,l) ->
118 7291cb80 xthirioux
      let c' = instantiate_carrier c inst_cr_vars in
119
      {ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)}
120 45f0f48d xthirioux
  | Cvar  -> ck
121 22fe1c93 ploc
  | Clink ck' ->
122 7291cb80 xthirioux
      {ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')}
123 22fe1c93 ploc
  | Ccarrying (cr,ck') ->
124 7291cb80 xthirioux
      let cr' = instantiate_carrier cr inst_cr_vars in
125 22fe1c93 ploc
        {ck with cdesc =
126 7291cb80 xthirioux
         Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')}
127 45f0f48d xthirioux
  | Cunivar ->
128 22fe1c93 ploc
      try
129
        List.assoc ck.cid !inst_ck_vars
130
      with Not_found ->
131 45f0f48d xthirioux
        let var = new_ck Cvar true in
132 22fe1c93 ploc
	inst_ck_vars := (ck.cid, var)::!inst_ck_vars;
133
	var
134
135
136
let rec update_scope_carrier scoped cr =
137
  if (not scoped) then
138
    begin
139
      cr.carrier_scoped <- scoped;
140
      match cr.carrier_desc with
141
	| Carry_const _ | Carry_name | Carry_var -> ()
142
      | Carry_link cr' -> update_scope_carrier scoped cr'
143
    end
144
145
let rec update_scope scoped ck =
146
  if (not scoped) then
147
    begin
148
      ck.cscoped <- scoped;
149
      match ck.cdesc with
150
      | Carrow (ck1,ck2) ->
151
          update_scope scoped ck1; update_scope scoped ck2
152
      | Ctuple clist ->
153
          List.iter (update_scope scoped) clist
154
      | Con (ck',cr,_) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*)
155 45f0f48d xthirioux
      | Cvar | Cunivar -> ()
156 22fe1c93 ploc
      | Clink ck' ->
157
          update_scope scoped ck'
158
      | Ccarrying (cr,ck') ->
159
          update_scope_carrier scoped cr; update_scope scoped ck'
160
    end
161
162
163
(* Unifies two clock carriers *)
164
let unify_carrier cr1 cr2 =
165
  let cr1 = carrier_repr cr1 in
166
  let cr2 = carrier_repr cr2 in
167 8a183477 xthirioux
  if cr1==cr2 then ()
168 22fe1c93 ploc
  else
169
    match cr1.carrier_desc, cr2.carrier_desc with
170
    | Carry_const id1, Carry_const id2 ->
171
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
172
    | Carry_const _, Carry_name ->
173
      begin
174
	cr2.carrier_desc <- Carry_link cr1;
175
	update_scope_carrier cr2.carrier_scoped cr1
176
      end
177
    | Carry_name, Carry_const _ ->
178
      begin
179
        cr1.carrier_desc <- Carry_link cr2;
180
        update_scope_carrier cr1.carrier_scoped cr2
181
      end
182
    | Carry_name, Carry_name ->
183
      if cr1.carrier_id < cr2.carrier_id then
184
        begin
185
          cr2.carrier_desc <- Carry_link cr1;
186
          update_scope_carrier cr2.carrier_scoped cr1
187
        end
188
      else
189
        begin
190
          cr1.carrier_desc <- Carry_link cr2;
191
          update_scope_carrier cr1.carrier_scoped cr2
192
        end
193 8f1c7e91 xthirioux
    | _,_ -> assert false
194
195
(* Semi-unifies two clock carriers *)
196
let semi_unify_carrier cr1 cr2 =
197
  let cr1 = carrier_repr cr1 in
198
  let cr2 = carrier_repr cr2 in
199 8a183477 xthirioux
  if cr1==cr2 then ()
200 8f1c7e91 xthirioux
  else
201
    match cr1.carrier_desc, cr2.carrier_desc with
202
    | Carry_const id1, Carry_const id2 ->
203
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
204
    | Carry_const _, Carry_name ->
205
      begin
206
	cr2.carrier_desc <- Carry_link cr1;
207
	update_scope_carrier cr2.carrier_scoped cr1
208
      end
209
    | Carry_name, Carry_const _ -> raise (Mismatch (cr1, cr2))
210
    | Carry_name, Carry_name ->
211
      if cr1.carrier_id < cr2.carrier_id then
212
        begin
213
          cr2.carrier_desc <- Carry_link cr1;
214
          update_scope_carrier cr2.carrier_scoped cr1
215
        end
216
      else
217
        begin
218
          cr1.carrier_desc <- Carry_link cr2;
219
          update_scope_carrier cr1.carrier_scoped cr2
220
        end
221
    | _,_ -> assert false
222 22fe1c93 ploc
223 6fdfb60b xthirioux
let try_unify_carrier ck1 ck2 loc =
224
  try
225
    unify_carrier ck1 ck2
226
  with
227
  | Unify (ck1',ck2') ->
228
    raise (Error (loc, Clock_clash (ck1',ck2')))
229
  | Mismatch (cr1,cr2) ->
230
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
231
232 22fe1c93 ploc
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify
233
    (ck1,ck2)] if the clocks are not unifiable.*)
234
let rec unify ck1 ck2 =
235
  let ck1 = repr ck1 in
236
  let ck2 = repr ck2 in
237 8a183477 xthirioux
  if ck1==ck2 then
238 22fe1c93 ploc
    ()
239
  else
240 45f0f48d xthirioux
    match ck1.cdesc,ck2.cdesc with
241
    | Cvar, Cvar ->
242
      if ck1.cid < ck2.cid then
243
        begin
244
          ck2.cdesc <- Clink (simplify ck1);
245
          update_scope ck2.cscoped ck1
246
        end
247
      else
248
        begin
249
          ck1.cdesc <- Clink (simplify ck2);
250
          update_scope ck1.cscoped ck2
251
        end
252
    | (Cvar, _) when (not (occurs ck1 ck2)) ->
253
      update_scope ck1.cscoped ck2;
254
      ck1.cdesc <- Clink (simplify ck2)
255
    | (_, Cvar) when (not (occurs ck2 ck1)) ->
256
      update_scope ck2.cscoped ck1;
257
      ck2.cdesc <- Clink (simplify ck1)
258
    | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
259
      unify_carrier cr1 cr2;
260
      unify ck1' ck2'
261
    | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
262
      raise (Unify (ck1,ck2))
263
    | Carrow (c1,c2), Carrow (c1',c2') ->
264
      unify c1 c1'; unify c2 c2'
265
    | Ctuple ckl1, Ctuple ckl2 ->
266
      if (List.length ckl1) <> (List.length ckl2) then
267
        raise (Unify (ck1,ck2));
268
      List.iter2 unify ckl1 ckl2
269
    | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
270
      unify_carrier c1 c2;
271
      unify ck' ck''
272
    | Cunivar, _ | _, Cunivar -> ()
273
    | _,_ -> raise (Unify (ck1,ck2))
274 8f1c7e91 xthirioux
275
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
276
    (ck1,ck2)] if the clocks are not semi-unifiable.*)
277
let rec semi_unify ck1 ck2 =
278
  let ck1 = repr ck1 in
279
  let ck2 = repr ck2 in
280 8a183477 xthirioux
  if ck1==ck2 then
281 8f1c7e91 xthirioux
    ()
282
  else
283
      match ck1.cdesc,ck2.cdesc with
284 45f0f48d xthirioux
      | Cvar, Cvar ->
285 8f1c7e91 xthirioux
          if ck1.cid < ck2.cid then
286
            begin
287
              ck2.cdesc <- Clink (simplify ck1);
288
              update_scope ck2.cscoped ck1
289
            end
290
          else
291
            begin
292
              ck1.cdesc <- Clink (simplify ck2);
293
              update_scope ck1.cscoped ck2
294
            end
295 45f0f48d xthirioux
      | (Cvar, _) -> raise (Unify (ck1,ck2))
296
      | (_, Cvar) when (not (occurs ck2 ck1)) ->
297 8f1c7e91 xthirioux
          update_scope ck2.cscoped ck1;
298
          ck2.cdesc <- Clink (simplify ck1)
299
      | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
300
          semi_unify_carrier cr1 cr2;
301
          semi_unify ck1' ck2'
302
      | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
303
          raise (Unify (ck1,ck2))
304
      | Carrow (c1,c2), Carrow (c1',c2') ->
305
	begin
306
          semi_unify c1 c1';
307
	  semi_unify c2 c2'
308
	end
309
      | Ctuple ckl1, Ctuple ckl2 ->
310
          if (List.length ckl1) <> (List.length ckl2) then
311
            raise (Unify (ck1,ck2));
312
          List.iter2 semi_unify ckl1 ckl2
313
      | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
314
          semi_unify_carrier c1 c2;
315
          semi_unify ck' ck''
316 45f0f48d xthirioux
      | Cunivar, _ | _, Cunivar -> ()
317 22fe1c93 ploc
      | _,_ -> raise (Unify (ck1,ck2))
318
319
(* Returns the value corresponding to a pclock (integer) factor
320
   expression. Expects a constant expression (checked by typing). *)
321
let int_factor_of_expr e =
322
  match e.expr_desc with 
323
  | Expr_const
324
      (Const_int i) -> i
325
  | _ -> failwith "Internal error: int_factor_of_expr"
326
327 54d032f5 xthirioux
(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *)
328
let rec clock_uncarry ck =
329 22fe1c93 ploc
  let ck = repr ck in
330
  match ck.cdesc with
331
  | Ccarrying (_, ck') -> ck'
332 54d032f5 xthirioux
  | Con(ck', cr, l)    -> clock_on (clock_uncarry ck') cr l
333
  | Ctuple ckl         -> clock_of_clock_list (List.map clock_uncarry ckl)
334 22fe1c93 ploc
  | _                  -> ck
335
336
let try_unify ck1 ck2 loc =
337
  try
338
    unify ck1 ck2
339
  with
340
  | Unify (ck1',ck2') ->
341
    raise (Error (loc, Clock_clash (ck1',ck2')))
342
  | Mismatch (cr1,cr2) ->
343
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
344
345 8f1c7e91 xthirioux
let try_semi_unify ck1 ck2 loc =
346
  try
347
    semi_unify ck1 ck2
348
  with
349
  | Unify (ck1',ck2') ->
350
    raise (Error (loc, Clock_clash (ck1',ck2')))
351
  | Mismatch (cr1,cr2) ->
352
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
353
354 6fdfb60b xthirioux
(* ck2 is a subtype of ck1 *)
355 52cfee34 xthirioux
let rec sub_unify sub ck1 ck2 =
356 22fe1c93 ploc
  match (repr ck1).cdesc, (repr ck2).cdesc with
357 52cfee34 xthirioux
  | Ctuple cl1         , Ctuple cl2         ->
358
    if List.length cl1 <> List.length cl2
359
    then raise (Unify (ck1, ck2))
360
    else List.iter2 (sub_unify sub) cl1 cl2
361
  | Ctuple [c1]        , _                  -> sub_unify sub c1 ck2
362
  | _                  , Ctuple [c2]        -> sub_unify sub ck1 c2
363
  | Con (c1, cr1, t1)  , Con (c2, cr2, t2) when t1=t2 ->
364
    begin
365
      unify_carrier cr1 cr2;
366
      sub_unify sub c1 c2
367
    end
368
  | Ccarrying (cr1, c1), Ccarrying (cr2, c2)->
369
    begin
370
      unify_carrier cr1 cr2;
371
      sub_unify sub c1 c2
372
    end
373 6fdfb60b xthirioux
  | _, Ccarrying (_, c2)           when sub -> sub_unify sub ck1 c2
374 52cfee34 xthirioux
  | _                                       -> unify ck1 ck2
375
376
let try_sub_unify sub ck1 ck2 loc =
377
  try
378
    sub_unify sub ck1 ck2
379
  with
380
  | Unify (ck1',ck2') ->
381
    raise (Error (loc, Clock_clash (ck1',ck2')))
382
  | Mismatch (cr1,cr2) ->
383
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
384 22fe1c93 ploc
385 45c13277 xthirioux
(* Unifies all the clock variables in the clock type of a tuple 
386
   expression, so that the clock type only uses at most one clock variable *)
387
let unify_tuple_clock ref_ck_opt ck loc =
388 6fdfb60b xthirioux
(*(match ref_ck_opt with
389
| None     -> Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck
390
  | Some ck' -> Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*)
391 45c13277 xthirioux
  let ck_var = ref ref_ck_opt in
392
  let rec aux ck =
393
    match (repr ck).cdesc with
394
    | Con _
395 45f0f48d xthirioux
    | Cvar ->
396 45c13277 xthirioux
        begin
397
          match !ck_var with
398
          | None ->
399
              ck_var:=Some ck
400
          | Some v ->
401
              (* may fail *)
402 6fdfb60b xthirioux
              try_unify ck v loc
403 45c13277 xthirioux
        end
404
    | Ctuple cl ->
405
        List.iter aux cl
406
    | Carrow _ -> assert false (* should not occur *)
407
    | Ccarrying (_, ck1) ->
408
        aux ck1
409
    | _ -> ()
410 6fdfb60b xthirioux
  in aux ck
411 45c13277 xthirioux
412
(* Unifies all the clock variables in the clock type of an imported
413
   node, so that the clock type only uses at most one base clock variable,
414
   that is, the activation clock of the node *)
415
let unify_imported_clock ref_ck_opt ck loc =
416
  let ck_var = ref ref_ck_opt in
417
  let rec aux ck =
418
    match (repr ck).cdesc with
419 45f0f48d xthirioux
    | Cvar ->
420 45c13277 xthirioux
        begin
421
          match !ck_var with
422
          | None ->
423
              ck_var:=Some ck
424
          | Some v ->
425
              (* cannot fail *)
426 6fdfb60b xthirioux
              try_unify ck v loc
427 45c13277 xthirioux
        end
428
    | Ctuple cl ->
429
        List.iter aux cl
430
    | Carrow (ck1,ck2) ->
431
        aux ck1; aux ck2
432
    | Ccarrying (_, ck1) ->
433
        aux ck1
434
    | Con (ck1, _, _) -> aux ck1
435
    | _ -> ()
436
  in
437
  aux ck
438
439 54d032f5 xthirioux
(* Computes the root clock of a tuple or a node clock,
440
   which is not the same as the base clock.
441
   Root clock will be used as the call clock 
442
   of a given node instance *)
443
let compute_root_clock ck =
444
  let root = Clocks.root ck in
445
  let branch = ref None in
446
  let rec aux ck =
447
    match (repr ck).cdesc with
448
    | Ctuple cl ->
449
        List.iter aux cl
450
    | Carrow (ck1,ck2) ->
451
        aux ck1; aux ck2
452
    | _ ->
453
        begin
454
          match !branch with
455
          | None ->
456
              branch := Some (Clocks.branch ck)
457
          | Some br ->
458
              (* cannot fail *)
459
              branch := Some (Clocks.common_prefix br (Clocks.branch ck))
460
        end
461
  in
462
  begin
463
    aux ck;
464
    Clocks.clock_of_root_branch root (Utils.desome !branch)
465
  end
466
467 22fe1c93 ploc
(* Clocks a list of arguments of Lustre builtin operators:
468
   - type each expression, remove carriers of clocks as
469
     carriers may only denote variables, not arbitrary expr.
470
   - try to unify these clocks altogether
471
*)
472
let rec clock_standard_args env expr_list =
473
  let ck_list = List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list in
474
  let ck_res = new_var true in
475
  List.iter2 (fun e ck -> try_unify ck ck_res e.expr_loc) expr_list ck_list;
476
  ck_res
477
478
(* emulates a subtyping relation between clocks c and (cr : c),
479
   used during node application only *)
480 52cfee34 xthirioux
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =
481 22fe1c93 ploc
  let loc = real_arg.expr_loc in
482
  let real_clock = clock_expr env real_arg in
483 74f1d8d3 xthirioux
  try_sub_unify sub formal_clock real_clock loc
484 22fe1c93 ploc
485
(* computes clocks for node application *)
486
and clock_appl env f args clock_reset loc =
487 b616fe7a xthirioux
 let args = expr_list_of_expr args in
488 04a63d25 xthirioux
  if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args
489 b616fe7a xthirioux
  then
490
      let args = Utils.transpose_list (List.map expr_list_of_expr args) in
491
      Clocks.clock_of_clock_list (List.map (fun args -> clock_call env f args clock_reset loc) args)
492
  else
493
    clock_call env f args clock_reset loc
494
495
and clock_call env f args clock_reset loc =
496 22fe1c93 ploc
  let cfun = clock_ident false env f loc in
497
  let cins, couts = split_arrow cfun in
498
  let cins = clock_list_of_clock cins in
499
  List.iter2 (clock_subtyping_arg env) args cins;
500 45c13277 xthirioux
  unify_imported_clock (Some clock_reset) cfun loc;
501 22fe1c93 ploc
  couts
502
503
and clock_ident nocarrier env id loc =
504
  clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)
505
506
and clock_carrier env c loc ce =
507
  let expr_c = expr_of_ident c loc in
508
  let ck = clock_expr ~nocarrier:false env expr_c in
509
  let cr = new_carrier Carry_name (*Carry_const c*) ck.cscoped in
510 6fdfb60b xthirioux
  let ckb = new_var true in
511
  let ckcarry = new_ck (Ccarrying (cr, ckb)) ck.cscoped in
512 22fe1c93 ploc
  try_unify ck ckcarry expr_c.expr_loc;
513 6fdfb60b xthirioux
  unify_tuple_clock (Some ckb) ce expr_c.expr_loc;
514
  cr
515 22fe1c93 ploc
516
(** [clock_expr env expr] performs the clock calculus for expression [expr] in
517
    environment [env] *)
518
and clock_expr ?(nocarrier=true) env expr =
519
  let resulting_ck = 
520
    match expr.expr_desc with
521
      | Expr_const cst ->
522
      let ck = new_var true in
523
      expr.expr_clock <- ck;
524
      ck
525
  | Expr_ident v ->
526
      let ckv =
527
        try
528
          Env.lookup_value env v
529
        with Not_found -> 
530
	  failwith ("Internal error, variable \""^v^"\" not found")
531
      in
532 7291cb80 xthirioux
      let ck = instantiate (ref []) (ref []) ckv in
533 22fe1c93 ploc
      expr.expr_clock <- ck;
534
      ck
535
  | Expr_array elist ->
536
    let ck = clock_standard_args env elist in
537
    expr.expr_clock <- ck;
538
    ck
539
  | Expr_access (e1, d) ->
540
    (* dimension, being a static value, doesn't need to be clocked *)
541
    let ck = clock_standard_args env [e1] in
542
    expr.expr_clock <- ck;
543
    ck
544
  | Expr_power (e1, d) ->
545
    (* dimension, being a static value, doesn't need to be clocked *)
546
    let ck = clock_standard_args env [e1] in
547
    expr.expr_clock <- ck;
548
    ck
549
  | Expr_tuple elist ->
550
    let ck = new_ck (Ctuple (List.map (clock_expr env) elist)) true in
551
    expr.expr_clock <- ck;
552
    ck
553
  | Expr_ite (c, t, e) ->
554
    let ck_c = clock_standard_args env [c] in
555
    let ck = clock_standard_args env [t; e] in
556
    (* Here, the branches may exhibit a tuple clock, not the condition *)
557 45c13277 xthirioux
    unify_tuple_clock (Some ck_c) ck expr.expr_loc;
558 22fe1c93 ploc
    expr.expr_clock <- ck;
559
    ck
560
  | Expr_appl (id, args, r) ->
561
    (try
562
(* for a modular compilation scheme, all inputs/outputs must share the same clock !
563
   this is also the reset clock !
564
*)
565
    let cr =
566
      match r with
567
      | None        -> new_var true
568 54d032f5 xthirioux
      | Some c      -> clock_standard_args env [c] in
569 b4d9710b xthirioux
    let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in
570 22fe1c93 ploc
    expr.expr_clock <- couts;
571
    couts
572
    with exn -> (
573
      Format.eprintf "Current expr: %a@." Printers.pp_expr expr; 
574
      raise exn
575
    ))
576
  | Expr_fby (e1,e2)
577
  | Expr_arrow (e1,e2) ->
578
    let ck = clock_standard_args env [e1; e2] in
579 45c13277 xthirioux
    unify_tuple_clock None ck expr.expr_loc;
580 22fe1c93 ploc
    expr.expr_clock <- ck;
581
    ck
582
  | Expr_pre e -> (* todo : deal with phases as in tail ? *)
583
      let ck = clock_standard_args env [e] in
584
      expr.expr_clock <- ck;
585
      ck
586
  | Expr_when (e,c,l) ->
587
      let ce = clock_standard_args env [e] in
588
      let c_loc = loc_of_cond expr.expr_loc c in
589 6fdfb60b xthirioux
      let cr = clock_carrier env c c_loc ce in
590
      let ck = clock_on ce cr l in
591 22fe1c93 ploc
      let cr' = new_carrier (Carry_const c) ck.cscoped in
592 6fdfb60b xthirioux
      let ck' = clock_on ce cr' l in
593 22fe1c93 ploc
      expr.expr_clock <- ck';
594
      ck
595
  | Expr_merge (c,hl) ->
596
      let cvar = new_var true in
597 6fdfb60b xthirioux
      let crvar = new_carrier Carry_name true in
598 54d032f5 xthirioux
      List.iter (fun (t, h) -> let ckh = clock_uncarry (clock_expr env h) in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;
599 6fdfb60b xthirioux
      let cr = clock_carrier env c expr.expr_loc cvar in
600
      try_unify_carrier cr crvar expr.expr_loc;
601 54d032f5 xthirioux
      let cres = clock_current ((snd (List.hd hl)).expr_clock) in
602
      expr.expr_clock <- cres;
603
      cres
604 22fe1c93 ploc
  in
605 b616fe7a xthirioux
  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck);
606 22fe1c93 ploc
  resulting_ck
607
608
let clock_of_vlist vars =
609
  let ckl = List.map (fun v -> v.var_clock) vars in
610
  clock_of_clock_list ckl
611
612
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
613
    environment [env] *)
614
let clock_eq env eq =
615
  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
616
  let ck_rhs = clock_expr env eq.eq_rhs in
617
  clock_subtyping_arg env expr_lhs ck_rhs
618
619
(* [clock_coreclock cck] returns the clock_expr corresponding to clock
620
    declaration [cck] *)
621
let clock_coreclock env cck id loc scoped =
622
  match cck.ck_dec_desc with
623
  | Ckdec_any -> new_var scoped
624
  | Ckdec_bool cl ->
625
      let temp_env = Env.add_value env id (new_var true) in
626
      (* We just want the id to be present in the environment *)
627
      let dummy_id_expr = expr_of_ident id loc in
628
      let when_expr =
629
        List.fold_left
630
          (fun expr (x,l) ->
631
                {expr_tag = new_tag ();
632
                 expr_desc = Expr_when (expr,x,l);
633
                 expr_type = Types.new_var ();
634
                 expr_clock = new_var scoped;
635
                 expr_delay = Delay.new_var ();
636
                 expr_loc = loc;
637
		 expr_annot = None})
638
          dummy_id_expr cl
639
      in
640
      clock_expr temp_env when_expr
641
642
(* Clocks a variable declaration *)
643
let clock_var_decl scoped env vdecl =
644
  let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in
645 89b9e25c xthirioux
  let ck =
646
(* WTF ????
647 22fe1c93 ploc
    if vdecl.var_dec_const
648
    then
649
      (try_generalize ck vdecl.var_loc; ck)
650
    else
651 89b9e25c xthirioux
 *)
652 6afa892a xthirioux
      if Types.get_clock_base_type vdecl.var_type <> None
653 89b9e25c xthirioux
      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
654
      else ck in
655 ec433d69 xthirioux
  (if vdecl.var_dec_const
656
   then match vdecl.var_dec_value with
657
   | None   -> ()
658
   | Some v ->
659
     begin
660
       let ck_static = clock_expr env v in
661
       try_unify ck ck_static v.expr_loc
662
     end);
663
  try_unify ck vdecl.var_clock vdecl.var_loc;
664 22fe1c93 ploc
  Env.add_value env vdecl.var_id ck
665
666
(* Clocks a variable declaration list *)
667
let clock_var_decl_list env scoped l =
668
  List.fold_left (clock_var_decl scoped) env l
669
670
(** [clock_node env nd] performs the clock-calculus for node [nd] in
671 89b9e25c xthirioux
    environment [env].
672
    Generalization of clocks wrt scopes follows this rule:
673
    - generalize inputs (unscoped).
674
    - generalize outputs. As they are scoped, only clocks coming from inputs
675
      are allowed to be generalized.
676
    - generalize locals. As outputs don't depend on them (checked the step before),
677
      they can be generalized. 
678
 *)
679 22fe1c93 ploc
let clock_node env loc nd =
680
  (* let is_main = nd.node_id = !Options.main_node in *)
681
  let new_env = clock_var_decl_list env false nd.node_inputs in
682
  let new_env = clock_var_decl_list new_env true nd.node_outputs in
683 d4807c3d xthirioux
  let new_env = clock_var_decl_list new_env true nd.node_locals in
684 333e3a25 ploc
  let eqs, auts = get_node_eqs nd in (* TODO XXX: perform the clocking on auts.
685
					For the moment, it is ignored *)
686
  List.iter (clock_eq new_env) eqs;
687 22fe1c93 ploc
  let ck_ins = clock_of_vlist nd.node_inputs in
688
  let ck_outs = clock_of_vlist nd.node_outputs in
689
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
690 45c13277 xthirioux
  unify_imported_clock None ck_node loc;
691 52cfee34 xthirioux
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
692 89b9e25c xthirioux
  (* Local variables may contain first-order carrier variables that should be generalized.
693
     That's not the case for types. *)
694 6afa892a xthirioux
  try_generalize ck_node loc;
695 333e3a25 ploc
  (*
696
    List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
697
    List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*)
698 d4807c3d xthirioux
  (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*)
699 22fe1c93 ploc
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
700 333e3a25 ploc
  (*  if (is_main && is_polymorphic ck_node) then
701
      raise (Error (loc,(Cannot_be_polymorphic ck_node)));
702
  *)
703 52cfee34 xthirioux
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
704 22fe1c93 ploc
  nd.node_clock <- ck_node;
705
  Env.add_value env nd.node_id ck_node
706
707
708
let check_imported_pclocks loc ck_node =
709
  let pck = ref None in
710
  let rec aux ck =
711
    match ck.cdesc with
712
    | Carrow (ck1,ck2) -> aux ck1; aux ck2
713
    | Ctuple cl -> List.iter aux cl
714
    | Con (ck',_,_) -> aux ck'
715
    | Clink ck' -> aux ck'
716
    | Ccarrying (_,ck') -> aux ck'
717 45f0f48d xthirioux
    | Cvar | Cunivar  ->
718 22fe1c93 ploc
        match !pck with
719
        | None -> ()
720
        | Some (_,_) ->
721
            raise (Error (loc, (Invalid_imported_clock ck_node)))
722
  in
723
  aux ck_node
724
725
let clock_imported_node env loc nd =
726
  let new_env = clock_var_decl_list env false nd.nodei_inputs in
727
  ignore(clock_var_decl_list new_env false nd.nodei_outputs);
728
  let ck_ins = clock_of_vlist nd.nodei_inputs in
729
  let ck_outs = clock_of_vlist nd.nodei_outputs in
730
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
731 45c13277 xthirioux
  unify_imported_clock None ck_node loc;
732 22fe1c93 ploc
  check_imported_pclocks loc ck_node;
733
  try_generalize ck_node loc;
734
  nd.nodei_clock <- ck_node;
735
  Env.add_value env nd.nodei_id ck_node
736
737 0d54d8a8 ploc
738
let new_env = clock_var_decl_list
739
              
740 ef34b4ae xthirioux
let clock_top_const env cdecl=
741
  let ck = new_var false in
742
  try_generalize ck cdecl.const_loc;
743
  Env.add_value env cdecl.const_id ck
744 22fe1c93 ploc
745 ef34b4ae xthirioux
let clock_top_consts env clist =
746
  List.fold_left clock_top_const env clist
747
 
748
let rec clock_top_decl env decl =
749 22fe1c93 ploc
  match decl.top_decl_desc with
750
  | Node nd ->
751
    clock_node env decl.top_decl_loc nd
752
  | ImportedNode nd ->
753
    clock_imported_node env decl.top_decl_loc nd
754 ef34b4ae xthirioux
  | Const c ->
755
    clock_top_const env c
756
  | TypeDef _ -> List.fold_left clock_top_decl env (consts_of_enum_type decl)
757
  | Open _    -> env
758 22fe1c93 ploc
759
let clock_prog env decls =
760 ef34b4ae xthirioux
  List.fold_left clock_top_decl env decls
761 22fe1c93 ploc
762 8f1c7e91 xthirioux
(* Once the Lustre program is fully clocked,
763
   we must get back to the original description of clocks,
764
   with constant parameters, instead of unifiable internal variables. *)
765
766
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions,
767
   i.e. replacing unifiable second_order variables with the original carrier names.
768
   Once restored in this formulation, clocks may be meaningfully printed.
769
*)
770
let uneval_vdecl_generics vdecl =
771 89b9e25c xthirioux
 (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*)
772 6afa892a xthirioux
 if Types.get_clock_base_type vdecl.var_type <> None
773 8f1c7e91 xthirioux
 then
774
   match get_carrier_name vdecl.var_clock with
775
   | None    -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false)
776
   | Some cr -> Clocks.uneval vdecl.var_id cr
777
778
let uneval_node_generics vdecls =
779
  List.iter uneval_vdecl_generics vdecls
780
781
let uneval_top_generics decl =
782
  match decl.top_decl_desc with
783
  | Node nd ->
784 89b9e25c xthirioux
      (* A node could contain first-order carrier variable in local vars. This is not the case for types. *)
785
      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
786 8f1c7e91 xthirioux
  | ImportedNode nd ->
787
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
788 ef34b4ae xthirioux
  | Const _
789 b1655a21 xthirioux
  | Open _
790 ef34b4ae xthirioux
  | TypeDef _ -> ()
791 8f1c7e91 xthirioux
792
let uneval_prog_generics prog =
793
 List.iter uneval_top_generics prog
794
795 7291cb80 xthirioux
let check_env_compat header declared computed =
796 8f1c7e91 xthirioux
  uneval_prog_generics header;
797 5c1184ad ploc
  Env.iter declared (fun k decl_clock_k -> 
798 7291cb80 xthirioux
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
799 8f1c7e91 xthirioux
    try_semi_unify decl_clock_k computed_c Location.dummy_loc
800 5c1184ad ploc
  ) 
801 22fe1c93 ploc
(* Local Variables: *)
802
(* compile-command:"make -C .." *)
803
(* End: *)