Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clock_calculus.ml @ ba2f9fa1

History | View | Annotate | Download (31.8 KB)

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