Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/clock_calculus.ml
6 6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7 7
(*  under the terms of the GNU Lesser General Public License        *)
8 8
(*  version 2.1.                                                    *)
9
(*                                                                  *) 
9
(*                                                                  *)
10 10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *) 
11
(*                                                                  *)
12 12
(********************************************************************)
13 13

  
14

  
15 14
(** Main clock-calculus module. Based on type inference algorithms with
16
  destructive unification. Uses a bit of subtyping for periodic clocks. *)
15
    destructive unification. Uses a bit of subtyping for periodic clocks. *)
17 16

  
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. *)
17
(* Though it shares similarities with the typing module, no code is shared.
18
   Simple environments, very limited identifier scoping, no identifier
19
   redefinition allowed. *)
21 20
open Utils
22 21
open Lustre_types
23 22
open Corelang
......
25 24

  
26 25
let loc_of_cond (_s, e) id =
27 26
  let pos_start =
28
    { e with Lexing.pos_cnum = e.Lexing.pos_cnum - (String.length id) }
27
    { e with Lexing.pos_cnum = e.Lexing.pos_cnum - String.length id }
29 28
  in
30 29
  pos_start, e
31 30

  
32
(** [occurs cvar ck] returns true if the clock variable [cvar] occurs in
33
    clock [ck]. False otherwise. *)
31
(** [occurs cvar ck] returns true if the clock variable [cvar] occurs in clock
32
    [ck]. False otherwise. *)
34 33
let rec occurs cvar ck =
35 34
  let ck = repr ck in
36 35
  match ck.cdesc with
37 36
  | Carrow (ck1, ck2) ->
38
      (occurs cvar ck1) || (occurs cvar ck2)
37
    occurs cvar ck1 || occurs cvar ck2
39 38
  | Ctuple ckl ->
40
      List.exists (occurs cvar) ckl
41
  | Con (ck',_,_) -> occurs cvar ck'
42
  | Cvar  -> ck=cvar
43
  | Cunivar   -> false
44
  | Clink ck' -> occurs cvar ck'
45
  | Ccarrying (_,ck') -> occurs cvar ck'
39
    List.exists (occurs cvar) ckl
40
  | Con (ck', _, _) ->
41
    occurs cvar ck'
42
  | Cvar ->
43
    ck = cvar
44
  | Cunivar ->
45
    false
46
  | Clink ck' ->
47
    occurs cvar ck'
48
  | Ccarrying (_, ck') ->
49
    occurs cvar ck'
46 50

  
47 51
(* Clocks generalization *)
48 52
let rec generalize_carrier cr =
49 53
  match cr.carrier_desc with
50
  | Carry_const _
51
  | Carry_name ->
52
    if cr.carrier_scoped then
53
      raise (Scope_carrier cr);
54
  | Carry_const _ | Carry_name ->
55
    if cr.carrier_scoped then raise (Scope_carrier cr);
54 56
    cr.carrier_desc <- Carry_var
55
  | Carry_var -> ()
56
  | Carry_link cr' -> generalize_carrier cr'
57
  | Carry_var ->
58
    ()
59
  | Carry_link cr' ->
60
    generalize_carrier cr'
57 61

  
58
(** Promote monomorphic clock variables to polymorphic clock variables. *)
59 62
(* Generalize by side-effects *)
63

  
64
(** Promote monomorphic clock variables to polymorphic clock variables. *)
60 65
let rec generalize ck =
61 66
  match ck.cdesc with
62
  | Carrow (ck1,ck2) ->
63
    generalize ck1; generalize ck2
67
  | Carrow (ck1, ck2) ->
68
    generalize ck1;
69
    generalize ck2
64 70
  | Ctuple clist ->
65 71
    List.iter generalize clist
66
  | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
72
  | Con (ck', cr, _) ->
73
    generalize ck';
74
    generalize_carrier cr
67 75
  | Cvar ->
68
    if ck.cscoped then
69
      raise (Scope_clock ck);
76
    if ck.cscoped then raise (Scope_clock ck);
70 77
    ck.cdesc <- Cunivar
71
  | Cunivar -> ()
78
  | Cunivar ->
79
    ()
72 80
  | Clink ck' ->
73 81
    generalize ck'
74
  | Ccarrying (cr,ck') ->
75
    generalize_carrier cr; generalize ck'
82
  | Ccarrying (cr, ck') ->
83
    generalize_carrier cr;
84
    generalize ck'
76 85

  
77 86
let try_generalize ck_node loc =
78
  try 
79
    generalize ck_node
80
  with
87
  try generalize ck_node with
81 88
  | Scope_carrier cr ->
82 89
    raise (Error (loc, Carrier_extrusion (ck_node, cr)))
83 90
  | Scope_clock ck ->
......
87 94
let instantiate_carrier cr inst_cr_vars =
88 95
  let cr = carrier_repr cr in
89 96
  match cr.carrier_desc with
90
  | Carry_const _
91
  | Carry_name -> cr
97
  | Carry_const _ | Carry_name ->
98
    cr
92 99
  | Carry_link _ ->
93
      failwith "Internal error"
94
  | Carry_var ->
95
      try
96
        List.assoc cr.carrier_id !inst_cr_vars
97
      with Not_found ->            
98
        let cr_var = new_carrier Carry_name true in
99
        inst_cr_vars := (cr.carrier_id,cr_var)::!inst_cr_vars;
100
        cr_var
100
    failwith "Internal error"
101
  | Carry_var -> (
102
    try List.assoc cr.carrier_id !inst_cr_vars
103
    with Not_found ->
104
      let cr_var = new_carrier Carry_name true in
105
      inst_cr_vars := (cr.carrier_id, cr_var) :: !inst_cr_vars;
106
      cr_var)
107

  
108
(* inst_ck_vars ensures that a polymorphic variable is instanciated with the
109
   same monomorphic variable if it occurs several times in the same type.
110
   inst_cr_vars is the same for carriers. *)
101 111

  
102 112
(** Downgrade polymorphic clock variables to monomorphic clock variables *)
103
(* inst_ck_vars ensures that a polymorphic variable is instanciated with
104
   the same monomorphic variable if it occurs several times in the same
105
   type. inst_cr_vars is the same for carriers. *)
106 113
let rec instantiate inst_ck_vars inst_cr_vars ck =
107 114
  match ck.cdesc with
108
  | Carrow (ck1,ck2) ->
109
      {ck with cdesc =
110
       Carrow ((instantiate inst_ck_vars inst_cr_vars ck1),
111
               (instantiate inst_ck_vars inst_cr_vars ck2))}
115
  | Carrow (ck1, ck2) ->
116
    {
117
      ck with
118
      cdesc =
119
        Carrow
120
          ( instantiate inst_ck_vars inst_cr_vars ck1,
121
            instantiate inst_ck_vars inst_cr_vars ck2 );
122
    }
112 123
  | Ctuple cklist ->
113
      {ck with cdesc = Ctuple 
114
         (List.map (instantiate inst_ck_vars inst_cr_vars) cklist)}
115
  | Con (ck',c,l) ->
116
      let c' = instantiate_carrier c inst_cr_vars in
117
      {ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)}
118
  | Cvar  -> ck
124
    {
125
      ck with
126
      cdesc = Ctuple (List.map (instantiate inst_ck_vars inst_cr_vars) cklist);
127
    }
128
  | Con (ck', c, l) ->
129
    let c' = instantiate_carrier c inst_cr_vars in
130
    { ck with cdesc = Con (instantiate inst_ck_vars inst_cr_vars ck', c', l) }
131
  | Cvar ->
132
    ck
119 133
  | Clink ck' ->
120
      {ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')}
121
  | Ccarrying (cr,ck') ->
122
      let cr' = instantiate_carrier cr inst_cr_vars in
123
        {ck with cdesc =
124
         Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')}
125
  | Cunivar ->
126
      try
127
        List.assoc ck.cid !inst_ck_vars
128
      with Not_found ->
129
        let var = new_ck Cvar true in
130
	inst_ck_vars := (ck.cid, var)::!inst_ck_vars;
131
	var
132

  
134
    { ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck') }
135
  | Ccarrying (cr, ck') ->
136
    let cr' = instantiate_carrier cr inst_cr_vars in
137
    {
138
      ck with
139
      cdesc = Ccarrying (cr', instantiate inst_ck_vars inst_cr_vars ck');
140
    }
141
  | Cunivar -> (
142
    try List.assoc ck.cid !inst_ck_vars
143
    with Not_found ->
144
      let var = new_ck Cvar true in
145
      inst_ck_vars := (ck.cid, var) :: !inst_ck_vars;
146
      var)
133 147

  
134 148
let rec update_scope_carrier scoped cr =
135
  if (not scoped) then
136
    begin
137
      cr.carrier_scoped <- scoped;
138
      match cr.carrier_desc with
139
	| Carry_const _ | Carry_name | Carry_var -> ()
140
      | Carry_link cr' -> update_scope_carrier scoped cr'
141
    end
149
  if not scoped then (
150
    cr.carrier_scoped <- scoped;
151
    match cr.carrier_desc with
152
    | Carry_const _ | Carry_name | Carry_var ->
153
      ()
154
    | Carry_link cr' ->
155
      update_scope_carrier scoped cr')
142 156

  
143 157
let rec update_scope scoped ck =
144
  if (not scoped) then
145
    begin
146
      ck.cscoped <- scoped;
147
      match ck.cdesc with
148
      | Carrow (ck1,ck2) ->
149
          update_scope scoped ck1; update_scope scoped ck2
150
      | Ctuple clist ->
151
          List.iter (update_scope scoped) clist
152
      | Con (ck', _, _) -> update_scope scoped ck'(*; update_scope_carrier scoped cr*)
153
      | Cvar | Cunivar -> ()
154
      | Clink ck' ->
155
          update_scope scoped ck'
156
      | Ccarrying (cr,ck') ->
157
          update_scope_carrier scoped cr; update_scope scoped ck'
158
    end
159

  
158
  if not scoped then (
159
    ck.cscoped <- scoped;
160
    match ck.cdesc with
161
    | Carrow (ck1, ck2) ->
162
      update_scope scoped ck1;
163
      update_scope scoped ck2
164
    | Ctuple clist ->
165
      List.iter (update_scope scoped) clist
166
    | Con (ck', _, _) ->
167
      update_scope scoped ck' (*; update_scope_carrier scoped cr*)
168
    | Cvar | Cunivar ->
169
      ()
170
    | Clink ck' ->
171
      update_scope scoped ck'
172
    | Ccarrying (cr, ck') ->
173
      update_scope_carrier scoped cr;
174
      update_scope scoped ck')
160 175

  
161 176
(* Unifies two clock carriers *)
162 177
let unify_carrier cr1 cr2 =
163 178
  let cr1 = carrier_repr cr1 in
164 179
  let cr2 = carrier_repr cr2 in
165
  if cr1==cr2 then ()
180
  if cr1 == cr2 then ()
166 181
  else
167 182
    match cr1.carrier_desc, cr2.carrier_desc with
168 183
    | Carry_const id1, Carry_const id2 ->
169 184
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
170 185
    | Carry_const _, Carry_name ->
171
      begin
172
	cr2.carrier_desc <- Carry_link cr1;
173
	update_scope_carrier cr2.carrier_scoped cr1
174
      end
186
      cr2.carrier_desc <- Carry_link cr1;
187
      update_scope_carrier cr2.carrier_scoped cr1
175 188
    | Carry_name, Carry_const _ ->
176
      begin
177
        cr1.carrier_desc <- Carry_link cr2;
178
        update_scope_carrier cr1.carrier_scoped cr2
179
      end
189
      cr1.carrier_desc <- Carry_link cr2;
190
      update_scope_carrier cr1.carrier_scoped cr2
180 191
    | Carry_name, Carry_name ->
181
      if cr1.carrier_id < cr2.carrier_id then
182
        begin
183
          cr2.carrier_desc <- Carry_link cr1;
184
          update_scope_carrier cr2.carrier_scoped cr1
185
        end
186
      else
187
        begin
188
          cr1.carrier_desc <- Carry_link cr2;
189
          update_scope_carrier cr1.carrier_scoped cr2
190
        end
191
    | _,_ -> assert false
192
      if cr1.carrier_id < cr2.carrier_id then (
193
        cr2.carrier_desc <- Carry_link cr1;
194
        update_scope_carrier cr2.carrier_scoped cr1)
195
      else (
196
        cr1.carrier_desc <- Carry_link cr2;
197
        update_scope_carrier cr1.carrier_scoped cr2)
198
    | _, _ ->
199
      assert false
192 200

  
193 201
(* Semi-unifies two clock carriers *)
194 202
let semi_unify_carrier cr1 cr2 =
195 203
  let cr1 = carrier_repr cr1 in
196 204
  let cr2 = carrier_repr cr2 in
197
  if cr1==cr2 then ()
205
  if cr1 == cr2 then ()
198 206
  else
199 207
    match cr1.carrier_desc, cr2.carrier_desc with
200 208
    | Carry_const id1, Carry_const id2 ->
201 209
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
202 210
    | Carry_const _, Carry_name ->
203
      begin
204
	cr2.carrier_desc <- Carry_link cr1;
205
	update_scope_carrier cr2.carrier_scoped cr1
206
      end
207
    | Carry_name, Carry_const _ -> raise (Mismatch (cr1, cr2))
211
      cr2.carrier_desc <- Carry_link cr1;
212
      update_scope_carrier cr2.carrier_scoped cr1
213
    | Carry_name, Carry_const _ ->
214
      raise (Mismatch (cr1, cr2))
208 215
    | Carry_name, Carry_name ->
209
      if cr1.carrier_id < cr2.carrier_id then
210
        begin
211
          cr2.carrier_desc <- Carry_link cr1;
212
          update_scope_carrier cr2.carrier_scoped cr1
213
        end
214
      else
215
        begin
216
          cr1.carrier_desc <- Carry_link cr2;
217
          update_scope_carrier cr1.carrier_scoped cr2
218
        end
219
    | _,_ -> assert false
216
      if cr1.carrier_id < cr2.carrier_id then (
217
        cr2.carrier_desc <- Carry_link cr1;
218
        update_scope_carrier cr2.carrier_scoped cr1)
219
      else (
220
        cr1.carrier_desc <- Carry_link cr2;
221
        update_scope_carrier cr1.carrier_scoped cr2)
222
    | _, _ ->
223
      assert false
220 224

  
221 225
let try_unify_carrier ck1 ck2 loc =
222
  try
223
    unify_carrier ck1 ck2
224
  with
225
  | Unify (ck1',ck2') ->
226
    raise (Error (loc, Clock_clash (ck1',ck2')))
227
  | Mismatch (cr1,cr2) ->
228
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
229

  
230
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify
231
    (ck1,ck2)] if the clocks are not unifiable.*)
226
  try unify_carrier ck1 ck2 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
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify (ck1,ck2)] if
233
    the clocks are not unifiable.*)
232 234
let rec unify ck1 ck2 =
233 235
  let ck1 = repr ck1 in
234 236
  let ck2 = repr ck2 in
235
  if ck1==ck2 then
236
    ()
237
  if ck1 == ck2 then ()
237 238
  else
238
    match ck1.cdesc,ck2.cdesc with
239
    match ck1.cdesc, ck2.cdesc with
239 240
    | Cvar, Cvar ->
240
      if ck1.cid < ck2.cid then
241
        begin
242
          ck2.cdesc <- Clink (simplify ck1);
243
          update_scope ck2.cscoped ck1
244
        end
245
      else
246
        begin
247
          ck1.cdesc <- Clink (simplify ck2);
248
          update_scope ck1.cscoped ck2
249
        end
250
    | (Cvar, _) when (not (occurs ck1 ck2)) ->
241
      if ck1.cid < ck2.cid then (
242
        ck2.cdesc <- Clink (simplify ck1);
243
        update_scope ck2.cscoped ck1)
244
      else (
245
        ck1.cdesc <- Clink (simplify ck2);
246
        update_scope ck1.cscoped ck2)
247
    | Cvar, _ when not (occurs ck1 ck2) ->
251 248
      update_scope ck1.cscoped ck2;
252 249
      ck1.cdesc <- Clink (simplify ck2)
253
    | (_, Cvar) when (not (occurs ck2 ck1)) ->
250
    | _, Cvar when not (occurs ck2 ck1) ->
254 251
      update_scope ck2.cscoped ck1;
255 252
      ck2.cdesc <- Clink (simplify ck1)
256
    | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
253
    | Ccarrying (cr1, ck1'), Ccarrying (cr2, ck2') ->
257 254
      unify_carrier cr1 cr2;
258 255
      unify ck1' ck2'
259
    | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
260
      raise (Unify (ck1,ck2))
261
    | Carrow (c1,c2), Carrow (c1',c2') ->
262
      unify c1 c1'; unify c2 c2'
256
    | Ccarrying (_, _), _ | _, Ccarrying (_, _) ->
257
      raise (Unify (ck1, ck2))
258
    | Carrow (c1, c2), Carrow (c1', c2') ->
259
      unify c1 c1';
260
      unify c2 c2'
263 261
    | Ctuple ckl1, Ctuple ckl2 ->
264
      if (List.length ckl1) <> (List.length ckl2) then
265
        raise (Unify (ck1,ck2));
262
      if List.length ckl1 <> List.length ckl2 then raise (Unify (ck1, ck2));
266 263
      List.iter2 unify ckl1 ckl2
267
    | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
264
    | Con (ck', c1, l1), Con (ck'', c2, l2) when l1 = l2 ->
268 265
      unify_carrier c1 c2;
269 266
      unify ck' ck''
270
    | Cunivar, _ | _, Cunivar -> ()
271
    | _,_ -> raise (Unify (ck1,ck2))
267
    | Cunivar, _ | _, Cunivar ->
268
      ()
269
    | _, _ ->
270
      raise (Unify (ck1, ck2))
272 271

  
273 272
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
274 273
    (ck1,ck2)] if the clocks are not semi-unifiable.*)
275 274
let rec semi_unify ck1 ck2 =
276 275
  let ck1 = repr ck1 in
277 276
  let ck2 = repr ck2 in
278
  if ck1==ck2 then
279
    ()
277
  if ck1 == ck2 then ()
280 278
  else
281
      match ck1.cdesc,ck2.cdesc with
282
      | Cvar, Cvar ->
283
          if ck1.cid < ck2.cid then
284
            begin
285
              ck2.cdesc <- Clink (simplify ck1);
286
              update_scope ck2.cscoped ck1
287
            end
288
          else
289
            begin
290
              ck1.cdesc <- Clink (simplify ck2);
291
              update_scope ck1.cscoped ck2
292
            end
293
      | (Cvar, _) -> raise (Unify (ck1,ck2))
294
      | (_, Cvar) when (not (occurs ck2 ck1)) ->
295
          update_scope ck2.cscoped ck1;
296
          ck2.cdesc <- Clink (simplify ck1)
297
      | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
298
          semi_unify_carrier cr1 cr2;
299
          semi_unify ck1' ck2'
300
      | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
301
          raise (Unify (ck1,ck2))
302
      | Carrow (c1,c2), Carrow (c1',c2') ->
303
	begin
304
          semi_unify c1 c1';
305
	  semi_unify c2 c2'
306
	end
307
      | Ctuple ckl1, Ctuple ckl2 ->
308
          if (List.length ckl1) <> (List.length ckl2) then
309
            raise (Unify (ck1,ck2));
310
          List.iter2 semi_unify ckl1 ckl2
311
      | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
312
          semi_unify_carrier c1 c2;
313
          semi_unify ck' ck''
314
      | Cunivar, _ | _, Cunivar -> ()
315
      | _,_ -> raise (Unify (ck1,ck2))
316

  
317
(* Returns the value corresponding to a pclock (integer) factor
318
   expression. Expects a constant expression (checked by typing). *)
279
    match ck1.cdesc, ck2.cdesc with
280
    | Cvar, Cvar ->
281
      if ck1.cid < ck2.cid then (
282
        ck2.cdesc <- Clink (simplify ck1);
283
        update_scope ck2.cscoped ck1)
284
      else (
285
        ck1.cdesc <- Clink (simplify ck2);
286
        update_scope ck1.cscoped ck2)
287
    | Cvar, _ ->
288
      raise (Unify (ck1, ck2))
289
    | _, Cvar when not (occurs ck2 ck1) ->
290
      update_scope ck2.cscoped ck1;
291
      ck2.cdesc <- Clink (simplify ck1)
292
    | Ccarrying (cr1, ck1'), Ccarrying (cr2, ck2') ->
293
      semi_unify_carrier cr1 cr2;
294
      semi_unify ck1' ck2'
295
    | Ccarrying (_, _), _ | _, Ccarrying (_, _) ->
296
      raise (Unify (ck1, ck2))
297
    | Carrow (c1, c2), Carrow (c1', c2') ->
298
      semi_unify c1 c1';
299
      semi_unify c2 c2'
300
    | Ctuple ckl1, Ctuple ckl2 ->
301
      if List.length ckl1 <> List.length ckl2 then raise (Unify (ck1, ck2));
302
      List.iter2 semi_unify ckl1 ckl2
303
    | Con (ck', c1, l1), Con (ck'', c2, l2) when l1 = l2 ->
304
      semi_unify_carrier c1 c2;
305
      semi_unify ck' ck''
306
    | Cunivar, _ | _, Cunivar ->
307
      ()
308
    | _, _ ->
309
      raise (Unify (ck1, ck2))
310

  
311
(* Returns the value corresponding to a pclock (integer) factor expression.
312
   Expects a constant expression (checked by typing). *)
319 313
let int_factor_of_expr e =
320
  match e.expr_desc with 
321
  | Expr_const
322
      (Const_int i) -> i
323
  | _ -> failwith "Internal error: int_factor_of_expr"
314
  match e.expr_desc with
315
  | Expr_const (Const_int i) ->
316
    i
317
  | _ ->
318
    failwith "Internal error: int_factor_of_expr"
324 319

  
325 320
(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *)
326 321
let rec clock_uncarry ck =
327 322
  let ck = repr ck in
328 323
  match ck.cdesc with
329
  | Ccarrying (_, ck') -> ck'
330
  | Con(ck', cr, l)    -> clock_on (clock_uncarry ck') cr l
331
  | Ctuple ckl         -> clock_of_clock_list (List.map clock_uncarry ckl)
332
  | _                  -> ck
324
  | Ccarrying (_, ck') ->
325
    ck'
326
  | Con (ck', cr, l) ->
327
    clock_on (clock_uncarry ck') cr l
328
  | Ctuple ckl ->
329
    clock_of_clock_list (List.map clock_uncarry ckl)
330
  | _ ->
331
    ck
333 332

  
334 333
let try_unify ck1 ck2 loc =
335
  try
336
    unify ck1 ck2
337
  with
338
  | Unify (ck1',ck2') ->
339
    raise (Error (loc, Clock_clash (ck1',ck2')))
340
  | Mismatch (cr1,cr2) ->
341
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
334
  try unify ck1 ck2 with
335
  | Unify (ck1', ck2') ->
336
    raise (Error (loc, Clock_clash (ck1', ck2')))
337
  | Mismatch (cr1, cr2) ->
338
    raise (Error (loc, Carrier_mismatch (cr1, cr2)))
342 339

  
343 340
let try_semi_unify ck1 ck2 loc =
344
  try
345
    semi_unify ck1 ck2
346
  with
347
  | Unify (ck1',ck2') ->
348
    raise (Error (loc, Clock_clash (ck1',ck2')))
349
  | Mismatch (cr1,cr2) ->
350
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
341
  try semi_unify ck1 ck2 with
342
  | Unify (ck1', ck2') ->
343
    raise (Error (loc, Clock_clash (ck1', ck2')))
344
  | Mismatch (cr1, cr2) ->
345
    raise (Error (loc, Carrier_mismatch (cr1, cr2)))
351 346

  
352 347
(* ck2 is a subtype of ck1 *)
353 348
let rec sub_unify sub ck1 ck2 =
354 349
  match (repr ck1).cdesc, (repr ck2).cdesc with
355
  | Ctuple cl1         , Ctuple cl2         ->
356
    if List.length cl1 <> List.length cl2
357
    then raise (Unify (ck1, ck2))
350
  | Ctuple cl1, Ctuple cl2 ->
351
    if List.length cl1 <> List.length cl2 then raise (Unify (ck1, ck2))
358 352
    else List.iter2 (sub_unify sub) cl1 cl2
359
  | Ctuple [c1]        , _                  -> sub_unify sub c1 ck2
360
  | _                  , Ctuple [c2]        -> sub_unify sub ck1 c2
361
  | Con (c1, cr1, t1)  , Con (c2, cr2, t2) when t1=t2 ->
362
    begin
363
      unify_carrier cr1 cr2;
364
      sub_unify sub c1 c2
365
    end
366
  | Ccarrying (cr1, c1), Ccarrying (cr2, c2)->
367
    begin
368
      unify_carrier cr1 cr2;
369
      sub_unify sub c1 c2
370
    end
371
  | _, Ccarrying (_, c2)           when sub -> sub_unify sub ck1 c2
372
  | _                                       -> unify ck1 ck2
353
  | Ctuple [ c1 ], _ ->
354
    sub_unify sub c1 ck2
355
  | _, Ctuple [ c2 ] ->
356
    sub_unify sub ck1 c2
357
  | Con (c1, cr1, t1), Con (c2, cr2, t2) when t1 = t2 ->
358
    unify_carrier cr1 cr2;
359
    sub_unify sub c1 c2
360
  | Ccarrying (cr1, c1), Ccarrying (cr2, c2) ->
361
    unify_carrier cr1 cr2;
362
    sub_unify sub c1 c2
363
  | _, Ccarrying (_, c2) when sub ->
364
    sub_unify sub ck1 c2
365
  | _ ->
366
    unify ck1 ck2
373 367

  
374 368
let try_sub_unify sub ck1 ck2 loc =
375
  try
376
    sub_unify sub ck1 ck2
377
  with
378
  | Unify (ck1',ck2') ->
379
    raise (Error (loc, Clock_clash (ck1',ck2')))
380
  | Mismatch (cr1,cr2) ->
381
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
382

  
383
(* Unifies all the clock variables in the clock type of a tuple 
384
   expression, so that the clock type only uses at most one clock variable *)
369
  try sub_unify sub ck1 ck2 with
370
  | Unify (ck1', ck2') ->
371
    raise (Error (loc, Clock_clash (ck1', ck2')))
372
  | Mismatch (cr1, cr2) ->
373
    raise (Error (loc, Carrier_mismatch (cr1, cr2)))
374

  
375
(* Unifies all the clock variables in the clock type of a tuple expression, so
376
   that the clock type only uses at most one clock variable *)
385 377
let unify_tuple_clock ref_ck_opt ck loc =
386
(*(match ref_ck_opt with
387
| None     -> Format.eprintf "unify_tuple_clock None %a@." Clocks.print_ck ck
388
  | Some ck' -> Format.eprintf "unify_tuple_clock (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*)
378
  (*(match ref_ck_opt with | None -> Format.eprintf "unify_tuple_clock None
379
    %a@." Clocks.print_ck ck | Some ck' -> Format.eprintf "unify_tuple_clock
380
    (Some %a) %a@." Clocks.print_ck ck' Clocks.print_ck ck);*)
389 381
  let ck_var = ref ref_ck_opt in
390 382
  let rec aux ck =
391 383
    match (repr ck).cdesc with
392
    | Con _
393
    | Cvar ->
394
        begin
395
          match !ck_var with
396
          | None ->
397
              ck_var:=Some ck
398
          | Some v ->
399
              (* may fail *)
400
              try_unify ck v loc
401
        end
384
    | Con _ | Cvar -> (
385
      match !ck_var with
386
      | None ->
387
        ck_var := Some ck
388
      | Some v ->
389
        (* may fail *)
390
        try_unify ck v loc)
402 391
    | Ctuple cl ->
403
        List.iter aux cl
404
    | Carrow _ -> assert false (* should not occur *)
392
      List.iter aux cl
393
    | Carrow _ ->
394
      assert false (* should not occur *)
405 395
    | Ccarrying (_, ck1) ->
406
        aux ck1
407
    | _ -> ()
408
  in aux ck
396
      aux ck1
397
    | _ ->
398
      ()
399
  in
400
  aux ck
409 401

  
410
(* Unifies all the clock variables in the clock type of an imported
411
   node, so that the clock type only uses at most one base clock variable,
412
   that is, the activation clock of the node *)
402
(* Unifies all the clock variables in the clock type of an imported node, so
403
   that the clock type only uses at most one base clock variable, that is, the
404
   activation clock of the node *)
413 405
let unify_imported_clock ref_ck_opt ck loc =
414 406
  let ck_var = ref ref_ck_opt in
415 407
  let rec aux ck =
416 408
    match (repr ck).cdesc with
417
    | Cvar ->
418
      begin
419
        match !ck_var with
420
        | None ->
421
          ck_var := Some ck
422
        | Some v ->
423
          (* cannot fail *)
424
          try_unify ck v loc
425
      end
409
    | Cvar -> (
410
      match !ck_var with
411
      | None ->
412
        ck_var := Some ck
413
      | Some v ->
414
        (* cannot fail *)
415
        try_unify ck v loc)
426 416
    | Ctuple cl ->
427 417
      List.iter aux cl
428
    | Carrow (ck1,ck2) ->
429
      aux ck1; aux ck2
418
    | Carrow (ck1, ck2) ->
419
      aux ck1;
420
      aux ck2
430 421
    | Ccarrying (_, ck1) ->
431 422
      aux ck1
432
    | Con (ck1, _, _) -> aux ck1
433
    | _ -> ()
423
    | Con (ck1, _, _) ->
424
      aux ck1
425
    | _ ->
426
      ()
434 427
  in
435 428
  aux ck
436 429

  
437
(* Computes the root clock of a tuple or a node clock,
438
   which is not the same as the base clock.
439
   Root clock will be used as the call clock 
440
   of a given node instance *)
430
(* Computes the root clock of a tuple or a node clock, which is not the same as
431
   the base clock. Root clock will be used as the call clock of a given node
432
   instance *)
441 433
let compute_root_clock ck =
442 434
  let root = Clocks.root ck in
443 435
  let branch = ref None in
444 436
  let rec aux ck =
445 437
    match (repr ck).cdesc with
446 438
    | Ctuple cl ->
447
        List.iter aux cl
448
    | Carrow (ck1,ck2) ->
449
        aux ck1; aux ck2
450
    | _ ->
451
        begin
452
          match !branch with
453
          | None ->
454
              branch := Some (Clocks.branch ck)
455
          | Some br ->
456
              (* cannot fail *)
457
              branch := Some (Clocks.common_prefix br (Clocks.branch ck))
458
        end
439
      List.iter aux cl
440
    | Carrow (ck1, ck2) ->
441
      aux ck1;
442
      aux ck2
443
    | _ -> (
444
      match !branch with
445
      | None ->
446
        branch := Some (Clocks.branch ck)
447
      | Some br ->
448
        (* cannot fail *)
449
        branch := Some (Clocks.common_prefix br (Clocks.branch ck)))
459 450
  in
460
  begin
461
    aux ck;
462
    Clocks.clock_of_root_branch root (Utils.desome !branch)
463
  end
464

  
465
(* Clocks a list of arguments of Lustre builtin operators:
466
   - type each expression, remove carriers of clocks as
467
     carriers may only denote variables, not arbitrary expr.
468
   - try to unify these clocks altogether
469
*)
451
  aux ck;
452
  Clocks.clock_of_root_branch root (Utils.desome !branch)
453

  
454
(* Clocks a list of arguments of Lustre builtin operators: - type each
455
   expression, remove carriers of clocks as carriers may only denote variables,
456
   not arbitrary expr. - try to unify these clocks altogether *)
470 457
let rec clock_standard_args env expr_list =
471
  let ck_list = List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list in
458
  let ck_list =
459
    List.map (fun e -> clock_uncarry (clock_expr env e)) expr_list
460
  in
472 461
  let ck_res = new_var true in
473 462
  List.iter2 (fun e ck -> try_unify ck ck_res e.expr_loc) expr_list ck_list;
474 463
  ck_res
475 464

  
476
(* emulates a subtyping relation between clocks c and (cr : c),
477
   used during node application only *)
478
and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =
465
(* emulates a subtyping relation between clocks c and (cr : c), used during node
466
   application only *)
467
and clock_subtyping_arg env ?(sub = true) real_arg formal_clock =
479 468
  let loc = real_arg.expr_loc in
480 469
  let real_clock = clock_expr env real_arg in
481 470
  try_sub_unify sub formal_clock real_clock loc
482 471

  
483 472
(* computes clocks for node application *)
484 473
and clock_appl env f args clock_reset loc =
485
 let args = expr_list_of_expr args in
486
  if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args
487
  then
488
      let args = Utils.transpose_list (List.map expr_list_of_expr args) in
489
      Clocks.clock_of_clock_list (List.map (fun args -> clock_call env f args clock_reset loc) args)
490
  else
491
    clock_call env f args clock_reset loc
474
  let args = expr_list_of_expr args in
475
  if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args then
476
    let args = Utils.transpose_list (List.map expr_list_of_expr args) in
477
    Clocks.clock_of_clock_list
478
      (List.map (fun args -> clock_call env f args clock_reset loc) args)
479
  else clock_call env f args clock_reset loc
492 480

  
493 481
and clock_call env f args clock_reset loc =
494 482
  (* Format.eprintf "Clocking call %s@." f; *)
......
500 488
  couts
501 489

  
502 490
and clock_ident nocarrier env id loc =
503
  clock_expr ~nocarrier:nocarrier env (expr_of_ident id loc)
491
  clock_expr ~nocarrier env (expr_of_ident id loc)
504 492

  
505 493
and clock_carrier env c loc ce =
506 494
  let expr_c = expr_of_ident c loc in
......
514 502

  
515 503
(** [clock_expr env expr] performs the clock calculus for expression [expr] in
516 504
    environment [env] *)
517
and clock_expr ?(nocarrier=true) env expr =
518
  let resulting_ck = 
505
and clock_expr ?(nocarrier = true) env expr =
506
  let resulting_ck =
519 507
    match expr.expr_desc with
520 508
    | Expr_const _ ->
521 509
      let ck = new_var true in
......
523 511
      ck
524 512
    | Expr_ident v ->
525 513
      let ckv =
526
        try
527
          Env.lookup_value env v
528
        with Not_found -> 
529
          failwith ("Internal error, variable \""^v^"\" not found")
514
        try Env.lookup_value env v
515
        with Not_found ->
516
          failwith ("Internal error, variable \"" ^ v ^ "\" not found")
530 517
      in
531 518
      let ck = instantiate (ref []) (ref []) ckv in
532 519
      expr.expr_clock <- ck;
......
537 524
      ck
538 525
    | Expr_access (e1, _) ->
539 526
      (* dimension, being a static value, doesn't need to be clocked *)
540
      let ck = clock_standard_args env [e1] in
527
      let ck = clock_standard_args env [ e1 ] in
541 528
      expr.expr_clock <- ck;
542 529
      ck
543 530
    | Expr_power (e1, _) ->
544 531
      (* dimension, being a static value, doesn't need to be clocked *)
545
      let ck = clock_standard_args env [e1] in
532
      let ck = clock_standard_args env [ e1 ] in
546 533
      expr.expr_clock <- ck;
547 534
      ck
548 535
    | Expr_tuple elist ->
......
550 537
      expr.expr_clock <- ck;
551 538
      ck
552 539
    | Expr_ite (c, t, e) ->
553
      let ck_c = clock_standard_args env [c] in
554
      let ck = clock_standard_args env [t; e] in
540
      let ck_c = clock_standard_args env [ c ] in
541
      let ck = clock_standard_args env [ t; e ] in
555 542
      (* Here, the branches may exhibit a tuple clock, not the condition *)
556 543
      unify_tuple_clock (Some ck_c) ck expr.expr_loc;
557 544
      expr.expr_clock <- ck;
558 545
      ck
559
    | Expr_appl (id, args, r) ->
560
      (try
561
         (* for a modular compilation scheme, all inputs/outputs must share the same clock !
562
            this is also the reset clock !
563
         *)
564
         let cr =
565
           match r with
566
           | None        -> new_var true
567
           | Some c      -> clock_standard_args env [c] in
568
         let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in
569
         expr.expr_clock <- couts;
570
         couts
571
       with exn -> (
572
           Format.eprintf "Current expr: %a@." Printers.pp_expr expr;
573
           raise exn
574
         ))
575
    | Expr_fby (e1,e2)
576
    | Expr_arrow (e1,e2) ->
577
      let ck = clock_standard_args env [e1; e2] in
546
    | Expr_appl (id, args, r) -> (
547
      try
548
        (* for a modular compilation scheme, all inputs/outputs must share the
549
           same clock ! this is also the reset clock ! *)
550
        let cr =
551
          match r with
552
          | None ->
553
            new_var true
554
          | Some c ->
555
            clock_standard_args env [ c ]
556
        in
557
        let couts = clock_appl env id args (clock_uncarry cr) expr.expr_loc in
558
        expr.expr_clock <- couts;
559
        couts
560
      with exn ->
561
        Format.eprintf "Current expr: %a@." Printers.pp_expr expr;
562
        raise exn)
563
    | Expr_fby (e1, e2) | Expr_arrow (e1, e2) ->
564
      let ck = clock_standard_args env [ e1; e2 ] in
578 565
      unify_tuple_clock None ck expr.expr_loc;
579 566
      expr.expr_clock <- ck;
580 567
      ck
581
    | Expr_pre e -> (* todo : deal with phases as in tail ? *)
582
      let ck = clock_standard_args env [e] in
568
    | Expr_pre e ->
569
      (* todo : deal with phases as in tail ? *)
570
      let ck = clock_standard_args env [ e ] in
583 571
      expr.expr_clock <- ck;
584 572
      ck
585
    | Expr_when (e,c,l) ->
586
      let ce = clock_standard_args env [e] in
573
    | Expr_when (e, c, l) ->
574
      let ce = clock_standard_args env [ e ] in
587 575
      let c_loc = loc_of_cond expr.expr_loc c in
588 576
      let cr = clock_carrier env c c_loc ce in
589 577
      let ck = clock_on ce cr l in
......
591 579
      let ck' = clock_on ce cr' l in
592 580
      expr.expr_clock <- ck';
593 581
      ck
594
    | Expr_merge (c,hl) ->
582
    | Expr_merge (c, hl) ->
595 583
      let cvar = new_var true in
596 584
      let crvar = new_carrier Carry_name true in
597
      List.iter (fun (t, h) ->
585
      List.iter
586
        (fun (t, h) ->
598 587
          let ckh = clock_uncarry (clock_expr env h) in
599
          unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;
588
          unify_tuple_clock
589
            (Some (new_ck (Con (cvar, crvar, t)) true))
590
            ckh h.expr_loc)
591
        hl;
600 592
      let cr = clock_carrier env c expr.expr_loc cvar in
601 593
      try_unify_carrier cr crvar expr.expr_loc;
602
      let cres = clock_current ((snd (List.hd hl)).expr_clock) in
594
      let cres = clock_current (snd (List.hd hl)).expr_clock in
603 595
      expr.expr_clock <- cres;
604 596
      cres
605 597
  in
606
  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@ "
607
                          Printers.pp_expr expr Clocks.print_ck resulting_ck);
598
  Log.report ~level:4 (fun fmt ->
599
      Format.fprintf fmt "Clock of expr %a: %a@ " Printers.pp_expr expr
600
        Clocks.print_ck resulting_ck);
608 601
  resulting_ck
609 602

  
610 603
let clock_of_vlist vars =
......
614 607
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
615 608
    environment [env] *)
616 609
let clock_eq env eq =
617
  let expr_lhs = expr_of_expr_list eq.eq_loc
618
      (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in
610
  let expr_lhs =
611
    expr_of_expr_list eq.eq_loc
612
      (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs)
613
  in
619 614
  let ck_rhs = clock_expr env eq.eq_rhs in
620 615
  clock_subtyping_arg env expr_lhs ck_rhs
621 616

  
622 617
(* [clock_coreclock cck] returns the clock_expr corresponding to clock
623
    declaration [cck] *)
618
   declaration [cck] *)
624 619
let clock_coreclock env cck id loc scoped =
625 620
  match cck.ck_dec_desc with
626
  | Ckdec_any -> new_var scoped
621
  | Ckdec_any ->
622
    new_var scoped
627 623
  | Ckdec_bool cl ->
628
      let temp_env = Env.add_value env id (new_var true) in
629
      (* We just want the id to be present in the environment *)
630
      let dummy_id_expr = expr_of_ident id loc in
631
      let when_expr =
632
        List.fold_left
633
          (fun expr (x,l) ->
634
                {expr_tag = new_tag ();
635
                 expr_desc = Expr_when (expr,x,l);
636
                 expr_type = Types.new_var ();
637
                 expr_clock = new_var scoped;
638
                 expr_delay = Delay.new_var ();
639
                 expr_loc = loc;
640
		 expr_annot = None})
641
          dummy_id_expr cl
642
      in
643
      clock_expr temp_env when_expr
624
    let temp_env = Env.add_value env id (new_var true) in
625
    (* We just want the id to be present in the environment *)
626
    let dummy_id_expr = expr_of_ident id loc in
627
    let when_expr =
628
      List.fold_left
629
        (fun expr (x, l) ->
630
          {
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
          })
639
        dummy_id_expr cl
640
    in
641
    clock_expr temp_env when_expr
644 642

  
645 643
(* Clocks a variable declaration *)
646 644
let clock_var_decl scoped env vdecl =
647
  let ck = clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped in
648 645
  let ck =
649
(* WTF ????
650
    if vdecl.var_dec_const
651
    then
652
      (try_generalize ck vdecl.var_loc; ck)
653
    else
654
 *)
655
      if Types.get_clock_base_type vdecl.var_type <> None
656
      then new_ck (Ccarrying (new_carrier Carry_name scoped, ck)) scoped
657
      else ck in
658
  (if vdecl.var_dec_const
659
   then match vdecl.var_dec_value with
660
   | None   -> ()
646
    clock_coreclock env vdecl.var_dec_clock vdecl.var_id vdecl.var_loc scoped
647
  in
648
  let ck =
649
    (* WTF ???? if vdecl.var_dec_const then (try_generalize ck vdecl.var_loc;
650
       ck) else *)
651
    if Types.get_clock_base_type vdecl.var_type <> None then
652
      new_ck (Ccarrying (new_carrier Carry_name scoped, ck)) scoped
653
    else ck
654
  in
655
  (if vdecl.var_dec_const then
656
   match vdecl.var_dec_value with
657
   | None ->
658
     ()
661 659
   | Some v ->
662
     begin
663
       let ck_static = clock_expr env v in
664
       try_unify ck ck_static v.expr_loc
665
     end);
660
     let ck_static = clock_expr env v in
661
     try_unify ck ck_static v.expr_loc);
666 662
  try_unify ck vdecl.var_clock vdecl.var_loc;
667 663
  Env.add_value env vdecl.var_id ck
668 664

  
......
670 666
let clock_var_decl_list env scoped l =
671 667
  List.fold_left (clock_var_decl scoped) env l
672 668

  
673
(** [clock_node env nd] performs the clock-calculus for node [nd] in
674
    environment [env].
675
    Generalization of clocks wrt scopes follows this rule:
676
    - generalize inputs (unscoped).
677
    - generalize outputs. As they are scoped, only clocks coming from inputs
678
      are allowed to be generalized.
679
    - generalize locals. As outputs don't depend on them (checked the step before),
680
      they can be generalized. 
681
 *)
669
(** [clock_node env nd] performs the clock-calculus for node [nd] in environment
670
    [env]. Generalization of clocks wrt scopes follows this rule: - generalize
671
    inputs (unscoped). - generalize outputs. As they are scoped, only clocks
672
    coming from inputs are allowed to be generalized. - generalize locals. As
673
    outputs don't depend on them (checked the step before), they can be
674
    generalized. *)
682 675
let clock_node env loc nd =
683 676
  (* let is_main = nd.node_id = !Options.main_node in *)
684 677
  let new_env = clock_var_decl_list env false nd.node_inputs in
685 678
  let new_env = clock_var_decl_list new_env true nd.node_outputs in
686 679
  let new_env = clock_var_decl_list new_env true nd.node_locals in
687
  let eqs, _ = get_node_eqs nd in (* TODO XXX: perform the clocking on auts.
688
					For the moment, it is ignored *)
680
  let eqs, _ = get_node_eqs nd in
681
  (* TODO XXX: perform the clocking on auts. For the moment, it is ignored *)
689 682
  List.iter (clock_eq new_env) eqs;
690 683
  let ck_ins = clock_of_vlist nd.node_inputs in
691 684
  let ck_outs = clock_of_vlist nd.node_outputs in
692 685
  let ck_node = new_ck (Carrow (ck_ins, ck_outs)) false in
693 686
  unify_imported_clock None ck_node loc;
694
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Clock of %s: %a@ " nd.node_id print_ck ck_node);
695
  (* Local variables may contain first-order carrier variables that should be generalized.
696
     That's not the case for types. *)
687
  Log.report ~level:3 (fun fmt ->
688
      Format.fprintf fmt "Clock of %s: %a@ " nd.node_id print_ck ck_node);
689
  (* Local variables may contain first-order carrier variables that should be
690
     generalized. That's not the case for types. *)
697 691
  try_generalize ck_node loc;
698
  (*
699
    List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
700
    List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*)
701
  (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*)
692
  (* List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc)
693
     nd.node_inputs; List.iter (fun vdecl -> try_generalize vdecl.var_clock
694
     vdecl.var_loc) nd.node_outputs;*)
695
  (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc)
696
    nd.node_locals;*)
702 697
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
703
  (*  if (is_main && is_polymorphic ck_node) then
704
      raise (Error (loc,(Cannot_be_polymorphic ck_node)));
705
  *)
706
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id print_ck ck_node);
698
  (* if (is_main && is_polymorphic ck_node) then raise (Error
699
     (loc,(Cannot_be_polymorphic ck_node))); *)
700
  Log.report ~level:3 (fun fmt ->
701
      Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id print_ck
702
        ck_node);
707 703
  nd.node_clock <- ck_node;
708 704
  Env.add_value env nd.node_id ck_node
709 705

  
710

  
711 706
let check_imported_pclocks loc ck_node =
712 707
  let pck = ref None in
713 708
  let rec aux ck =
714 709
    match ck.cdesc with
715
    | Carrow (ck1,ck2) -> aux ck1; aux ck2
716
    | Ctuple cl -> List.iter aux cl
717
    | Con (ck',_,_) -> aux ck'
718
    | Clink ck' -> aux ck'
719
    | Ccarrying (_,ck') -> aux ck'
720
    | Cvar | Cunivar  ->
721
        match !pck with
722
        | None -> ()
723
        | Some (_,_) ->
724
            raise (Error (loc, (Invalid_imported_clock ck_node)))
710
    | Carrow (ck1, ck2) ->
711
      aux ck1;
712
      aux ck2
713
    | Ctuple cl ->
714
      List.iter aux cl
715
    | Con (ck', _, _) ->
716
      aux ck'
717
    | Clink ck' ->
718
      aux ck'
719
    | Ccarrying (_, ck') ->
720
      aux ck'
721
    | Cvar | Cunivar -> (
722
      match !pck with
723
      | None ->
724
        ()
725
      | Some (_, _) ->
726
        raise (Error (loc, Invalid_imported_clock ck_node)))
725 727
  in
726 728
  aux ck_node
727 729

  
728 730
let clock_imported_node env loc nd =
729 731
  let new_env = clock_var_decl_list env false nd.nodei_inputs in
730
  ignore(clock_var_decl_list new_env false nd.nodei_outputs);
732
  ignore (clock_var_decl_list new_env false nd.nodei_outputs);
731 733
  let ck_ins = clock_of_vlist nd.nodei_inputs in
732 734
  let ck_outs = clock_of_vlist nd.nodei_outputs in
733
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
735
  let ck_node = new_ck (Carrow (ck_ins, ck_outs)) false in
734 736
  unify_imported_clock None ck_node loc;
735 737
  check_imported_pclocks loc ck_node;
736 738
  try_generalize ck_node loc;
737 739
  nd.nodei_clock <- ck_node;
738 740
  Env.add_value env nd.nodei_id ck_node
739 741

  
740

  
741 742
let new_env = clock_var_decl_list
742
              
743
let clock_top_const env cdecl=
743

  
744
let clock_top_const env cdecl =
744 745
  let ck = new_var false in
745 746
  try_generalize ck cdecl.const_loc;
746 747
  Env.add_value env cdecl.const_id ck
747 748

  
748
let clock_top_consts env clist =
749
  List.fold_left clock_top_const env clist
750
 
749
let clock_top_consts env clist = List.fold_left clock_top_const env clist
750

  
751 751
let rec clock_top_decl env decl =
752 752
  match decl.top_decl_desc with
753 753
  | Node nd ->
......
756 756
    clock_imported_node env decl.top_decl_loc nd
757 757
  | Const c ->
758 758
    clock_top_const env c
759
  | TypeDef _ -> List.fold_left clock_top_decl env (consts_of_enum_type decl)
760
  | Include _ | Open _    -> env
759
  | TypeDef _ ->
760
    List.fold_left clock_top_decl env (consts_of_enum_type decl)
761
  | Include _ | Open _ ->
762
    env
761 763

  
762
let clock_prog env decls =
763
  List.fold_left clock_top_decl env decls
764
let clock_prog env decls = List.fold_left clock_top_decl env decls
764 765

  
765
(* Once the Lustre program is fully clocked,
766
   we must get back to the original description of clocks,
767
   with constant parameters, instead of unifiable internal variables. *)
766
(* Once the Lustre program is fully clocked, we must get back to the original
767
   description of clocks, with constant parameters, instead of unifiable
768
   internal variables. *)
768 769

  
769
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions,
770
   i.e. replacing unifiable second_order variables with the original carrier names.
771
   Once restored in this formulation, clocks may be meaningfully printed.
772
*)
770
(* The following functions aims at 'unevaluating' carriers occuring in clock
771
   expressions, i.e. replacing unifiable second_order variables with the
772
   original carrier names. Once restored in this formulation, clocks may be
773
   meaningfully printed. *)
773 774
let uneval_vdecl_generics vdecl =
774
 (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*)
775
 if Types.get_clock_base_type vdecl.var_type <> None
776
 then
777
   match get_carrier_name vdecl.var_clock with
778
   | None    -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false)
779
   | Some cr -> Clocks.uneval vdecl.var_id cr
780

  
781
let uneval_node_generics vdecls =
782
  List.iter uneval_vdecl_generics vdecls
775
  (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@."
776
    Printers.pp_node_var vdecl;*)
777
  if Types.get_clock_base_type vdecl.var_type <> None then
778
    match get_carrier_name vdecl.var_clock with
779
    | None ->
780
      Format.eprintf "internal error: %a@." print_ck vdecl.var_clock;
781
      assert false
782
    | Some cr ->
783
      Clocks.uneval vdecl.var_id cr
784

  
785
let uneval_node_generics vdecls = List.iter uneval_vdecl_generics vdecls
783 786

  
784 787
let uneval_top_generics decl =
785 788
  match decl.top_decl_desc with
786 789
  | Node nd ->
787
      (* A node could contain first-order carrier variable in local vars. This is not the case for types. *)
788
      uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
790
    (* A node could contain first-order carrier variable in local vars. This is
791
       not the case for types. *)
792
    uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
789 793
  | ImportedNode nd ->
790
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
791
  | Const _
792
  | Include _ | Open _
793
  | TypeDef _ -> ()
794
    uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
795
  | Const _ | Include _ | Open _ | TypeDef _ ->
796
    ()
794 797

  
795
let uneval_prog_generics prog =
796
 List.iter uneval_top_generics prog
798
let uneval_prog_generics prog = List.iter uneval_top_generics prog
797 799

  
798 800
let check_env_compat header declared computed =
799 801
  uneval_prog_generics header;
800 802
  Env.iter declared (fun k decl_clock_k ->
801 803
      try
802
        let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
804
        let computed_c =
805
          instantiate (ref []) (ref []) (Env.lookup_value computed k)
806
        in
803 807
        try_semi_unify decl_clock_k computed_c Location.dummy_loc
804
      with Not_found -> (* If the lookup failed then either an actual
805
                           required element should have been declared
806
                           and is missing but typing should have catch
807
                           it, or it was a contract and does not
808
                           require this additional check.  *)
809
          ()
810
    ) 
808
      with Not_found ->
809
        (* If the lookup failed then either an actual required element should
810
           have been declared and is missing but typing should have catch it, or
811
           it was a contract and does not require this additional check. *)
812
        ())
811 813
(* Local Variables: *)
812 814
(* compile-command:"make -C .." *)
813 815
(* End: *)

Also available in: Unified diff