Project

General

Profile

Revision 45f0f48d

View differences:

lustrec.odocl
7 7
backends/C/C_backend_makefile
8 8
backends/C/C_backend_spec
9 9
backends/C/C_backend_src
10
backends/Horn/Horn_backend_common
11
backends/Horn/Horn_backend_printers
12
backends/Horn/Horn_backend_collecting_sem
10 13
backends/Horn/Horn_backend
11 14
plugins/scopes/Scopes
12 15
Basic_library
src/backends/C/c_backend_common.ml
182 182
  | Cst c         -> pp_c_const fmt c
183 183
  | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
184 184
  | Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
185
  | Power (v, n)  -> assert false
185
  | Power (v, n)  -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." pp_val v; assert false)
186 186
  | LocalVar v    -> pp_var fmt v
187 187
  | StateVar v    ->
188 188
    (* array memory vars are represented by an indirection to a local var with the right type,
src/backends/C/c_backend_makefile.ml
70 70
  fprintf fmt "@.";
71 71

  
72 72
  (* Main binary *)
73
  fprintf fmt "%s_%s:@." basename nodename;
73
  fprintf fmt "%s_%s: %s.c %s_main.c@." basename nodename basename basename;
74 74
  fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s.c@." basename;  
75 75
  fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s_main.c@." basename;   
76 76
  fprintf_dependencies fmt dependencies;    
src/backends/C/c_backend_src.ml
325 325

  
326 326
and pp_machine_instr dependencies (m: machine_t) self fmt instr =
327 327
  match instr with 
328
  | MNoReset _ -> ()
328 329
  | MReset i ->
329 330
    pp_machine_reset m self fmt i
330 331
  | MLocalAssign (i,v) ->
......
361 362
	(pp_c_val self (pp_c_var_read m)) g
362 363
	(Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl
363 364
  | MComment s  -> 
364
      fprintf fmt "//%s@ " s
365
      fprintf fmt "/*%s*/@ " s
365 366

  
366 367

  
367 368
and pp_machine_branch dependencies m self fmt (t, h) =
src/backends/Horn/horn_backend_printers.ml
42 42
let rec pp_horn_const fmt c =
43 43
  match c with
44 44
    | Const_int i    -> pp_print_int fmt i
45
    | Const_real (_,_s)   -> pp_print_string fmt s
45
    | Const_real (_,_,s)   -> pp_print_string fmt s
46 46
    | Const_tag t    -> pp_horn_tag fmt t
47 47
    | _              -> assert false
48 48

  
......
51 51
   but an offset suffix may be added for array variables
52 52
*)
53 53
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
54
  match v with
54
  match v.value_desc with
55 55
    | Cst c         -> pp_horn_const fmt c
56 56
    | Array _
57 57
    | Access _ -> assert false (* no arrays *)
......
65 65

  
66 66
(* Prints a [value] indexed by the suffix list [loop_vars] *)
67 67
let rec pp_value_suffix self pp_value fmt value =
68
 match value with
68
 match value.value_desc with
69 69
 | Fun (n, vl)  ->
70 70
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
71 71
 |  _            ->
......
77 77
   - [value]: assigned value
78 78
   - [pp_var]: printer for variables
79 79
*)
80
let pp_assign m pp_var fmt var_type var_name value =
80
let pp_assign m pp_var fmt var_name value =
81 81
  let self = m.mname.node_id in
82 82
  fprintf fmt "(= %a %a)" 
83 83
    (pp_horn_val ~is_lhs:true self pp_var) var_name
......
156 156
      | "_arrow", [i1; i2], [o], [mem_m], [mem_x] -> begin
157 157
	fprintf fmt "@[<v 5>(and ";
158 158
	fprintf fmt "(= %a (ite %a %a %a))"
159
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (LocalVar o) (* output var *)
159
	  (pp_horn_val ~is_lhs:true self (pp_horn_var m)) (mk_val (LocalVar o) o.var_type) (* output var *)
160 160
	  (pp_horn_var m) mem_m 
161 161
	  (pp_horn_val self (pp_horn_var m)) i1
162 162
	  (pp_horn_val self (pp_horn_var m)) i2
......
172 172
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m))) inputs
173 173
	  (Utils.pp_final_char_if_non_empty "@ " inputs)
174 174
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
175
	  (List.map (fun v -> LocalVar v) outputs)
175
	  (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
176 176
	  (Utils.pp_final_char_if_non_empty "@ " outputs)
177 177
	  (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (mid_mems@next_mems)
178 178
	
......
186 186
      inputs
187 187
      (Utils.pp_final_char_if_non_empty "@ " inputs)
188 188
      (Utils.fprintf_list ~sep:"@ " (pp_horn_val self (pp_horn_var m)))
189
      (List.map (fun v -> LocalVar v) outputs)
189
      (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
190 190
  )
191 191
    
192 192
    
......
202 202
  | MLocalAssign (i,v) ->
203 203
    pp_assign
204 204
      m (pp_horn_var m) fmt
205
      i.var_type (LocalVar i) v;
205
      (mk_val (LocalVar i) i.var_type) v;
206 206
    reset_instances
207 207
  | MStateAssign (i,v) ->
208 208
    pp_assign
209 209
      m (pp_horn_var m) fmt
210
      i.var_type (StateVar i) v;
210
      (mk_val (StateVar i) i.var_type) v;
211 211
    reset_instances
212
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i  ->
212
  | MStep ([i0], i, vl) when Basic_library.is_internal_fun i (List.map (fun v -> v.value_type) vl) ->
213 213
    assert false (* This should not happen anymore *)
214 214
  | MStep (il, i, vl) ->
215 215
    (* if reset instance, just print the call over mem_m , otherwise declare mem_m =
src/clock_calculus.ml
42 42
  | Ctuple ckl ->
43 43
      List.exists (occurs cvar) ckl
44 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
45
  | Cvar  -> ck=cvar
46
  | Cunivar   -> false
50 47
  | Clink ck' -> occurs cvar ck'
51 48
  | Ccarrying (_,ck') -> occurs cvar ck'
52 49

  
......
70 67
    | Ctuple clist ->
71 68
        List.iter generalize clist
72 69
    | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
73
    | Cvar cset ->
70
    | Cvar ->
74 71
        if ck.cscoped then
75 72
          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 _ -> ()
73
        ck.cdesc <- Cunivar 
74
    | Cunivar -> () 
81 75
    | Clink ck' ->
82 76
        generalize ck'
83 77
    | Ccarrying (cr,ck') ->
......
123 117
  | Con (ck',c,l) ->
124 118
      let c' = instantiate_carrier c inst_cr_vars in
125 119
      {ck with cdesc = Con ((instantiate inst_ck_vars inst_cr_vars ck'),c',l)}
126
  | Cvar _ | Pck_const (_,_) -> ck
127
  | Pck_up (ck',k) ->
128
      {ck with cdesc = Pck_up ((instantiate inst_ck_vars inst_cr_vars ck'),k)}
129
  | Pck_down (ck',k) ->
130
      {ck with cdesc = Pck_down ((instantiate inst_ck_vars inst_cr_vars ck'),k)}
131
  | Pck_phase (ck',q) ->
132
      {ck with cdesc = Pck_phase ((instantiate inst_ck_vars inst_cr_vars ck'),q)}
120
  | Cvar  -> ck
133 121
  | Clink ck' ->
134 122
      {ck with cdesc = Clink (instantiate inst_ck_vars inst_cr_vars ck')}
135 123
  | Ccarrying (cr,ck') ->
136 124
      let cr' = instantiate_carrier cr inst_cr_vars in
137 125
        {ck with cdesc =
138 126
         Ccarrying (cr',instantiate inst_ck_vars inst_cr_vars ck')}
139
  | Cunivar cset ->
127
  | Cunivar ->
140 128
      try
141 129
        List.assoc ck.cid !inst_ck_vars
142 130
      with Not_found ->
143
        let var = new_ck (Cvar cset) true in
131
        let var = new_ck Cvar true in
144 132
	inst_ck_vars := (ck.cid, var)::!inst_ck_vars;
145 133
	var
146 134

  
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 135

  
180 136
let rec update_scope_carrier scoped cr =
181 137
  if (not scoped) then
......
196 152
      | Ctuple clist ->
197 153
          List.iter (update_scope scoped) clist
198 154
      | 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 _ -> ()
155
      | Cvar | Cunivar -> ()
205 156
      | Clink ck' ->
206 157
          update_scope scoped ck'
207 158
      | Ccarrying (cr,ck') ->
208 159
          update_scope_carrier scoped cr; update_scope scoped ck'
209 160
    end
210 161

  
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 162

  
216 163
(* Unifies two clock carriers *)
217 164
let unify_carrier cr1 cr2 =
......
279 226
  with
280 227
  | Unify (ck1',ck2') ->
281 228
    raise (Error (loc, Clock_clash (ck1',ck2')))
282
  | Subsume (ck,cset) ->
283
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
284 229
  | Mismatch (cr1,cr2) ->
285 230
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
286 231

  
......
292 237
  if ck1==ck2 then
293 238
    ()
294 239
  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
      | Cunivar _, _ | _, Cunivar _ -> ()
390
      | _,_ -> raise (Unify (ck1,ck2))
240
    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))
391 274

  
392 275
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
393 276
    (ck1,ck2)] if the clocks are not semi-unifiable.*)
......
398 281
    ()
399 282
  else
400 283
      match ck1.cdesc,ck2.cdesc with
401
      | Cvar cset1,Cvar cset2->
284
      | Cvar, Cvar ->
402 285
          if ck1.cid < ck2.cid then
403 286
            begin
404 287
              ck2.cdesc <- Clink (simplify ck1);
......
409 292
              ck1.cdesc <- Clink (simplify ck2);
410 293
              update_scope ck1.cscoped ck2
411 294
            end
412
      | (Cvar cset,_) -> raise (Unify (ck1,ck2))
413
      | (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
295
      | (Cvar, _) -> raise (Unify (ck1,ck2))
296
      | (_, Cvar) when (not (occurs ck2 ck1)) ->
414 297
          update_scope ck2.cscoped ck1;
415 298
          ck2.cdesc <- Clink (simplify ck1)
416 299
      | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
......
430 313
      | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
431 314
          semi_unify_carrier c1 c2;
432 315
          semi_unify ck' ck''
433
      | Cunivar _, _ | _, Cunivar _ -> ()
316
      | Cunivar, _ | _, Cunivar -> ()
434 317
      | _,_ -> raise (Unify (ck1,ck2))
435 318

  
436 319
(* Returns the value corresponding to a pclock (integer) factor
......
456 339
  with
457 340
  | Unify (ck1',ck2') ->
458 341
    raise (Error (loc, Clock_clash (ck1',ck2')))
459
  | Subsume (ck,cset) ->
460
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
461 342
  | Mismatch (cr1,cr2) ->
462 343
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
463 344

  
......
467 348
  with
468 349
  | Unify (ck1',ck2') ->
469 350
    raise (Error (loc, Clock_clash (ck1',ck2')))
470
  | Subsume (ck,cset) ->
471
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
472 351
  | Mismatch (cr1,cr2) ->
473 352
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
474 353

  
......
500 379
  with
501 380
  | Unify (ck1',ck2') ->
502 381
    raise (Error (loc, Clock_clash (ck1',ck2')))
503
  | Subsume (ck,cset) ->
504
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
505 382
  | Mismatch (cr1,cr2) ->
506 383
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
507 384

  
......
515 392
  let rec aux ck =
516 393
    match (repr ck).cdesc with
517 394
    | Con _
518
    | Cvar _ ->
395
    | Cvar ->
519 396
        begin
520 397
          match !ck_var with
521 398
          | None ->
......
539 416
  let ck_var = ref ref_ck_opt in
540 417
  let rec aux ck =
541 418
    match (repr ck).cdesc with
542
    | Cvar _ ->
419
    | Cvar ->
543 420
        begin
544 421
          match !ck_var with
545 422
          | None ->
......
744 621
let clock_coreclock env cck id loc scoped =
745 622
  match cck.ck_dec_desc with
746 623
  | 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 624
  | Ckdec_bool cl ->
752 625
      let temp_env = Env.add_value env id (new_var true) in
753 626
      (* We just want the id to be present in the environment *)
......
837 710
    | Carrow (ck1,ck2) -> aux ck1; aux ck2
838 711
    | Ctuple cl -> List.iter aux cl
839 712
    | Con (ck',_,_) -> aux ck'
840
    | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) -> 
841
        raise (Error (loc, (Invalid_imported_clock ck_node)))
842
    | Pck_const (n,p) ->
843
        begin
844
          match !pck with
845
          | None -> pck := Some (n,p)
846
          | Some (n',p') ->
847
              if (n,p) <> (n',p') then
848
                raise (Error (loc, (Invalid_imported_clock ck_node)))
849
        end
850 713
    | Clink ck' -> aux ck'
851 714
    | Ccarrying (_,ck') -> aux ck'
852
    | Cvar _ | Cunivar _ ->
715
    | Cvar | Cunivar  ->
853 716
        match !pck with
854 717
        | None -> ()
855 718
        | Some (_,_) ->
src/clocks.ml
15 15
open Utils
16 16
open Format
17 17

  
18
(* Clock type sets, for subtyping. *)
19
type clock_set =
20
    CSet_all
21
  | CSet_pck of int*rat
18
(* (\* Clock type sets, for subtyping. *\) *)
19
(* type clock_set = *)
20
(*     CSet_all *)
21
(*   | CSet_pck of int*rat *)
22 22

  
23 23
(* Clock carriers basically correspond to the "c" in "x when c" *)
24 24
type carrier_desc =
......
44 44
  | Carrow of clock_expr * clock_expr
45 45
  | Ctuple of clock_expr list
46 46
  | Con of clock_expr * carrier_expr * ident
47
  | Pck_up of clock_expr * int
48
  | Pck_down of clock_expr * int
49
  | Pck_phase of clock_expr * rat
50
  | Pck_const of int * rat
51
  | Cvar of clock_set (* Monomorphic clock variable *)
52
  | Cunivar of clock_set (* Polymorphic clock variable *)
47
  (* | Pck_up of clock_expr * int *)
48
  (* | Pck_down of clock_expr * int *)
49
  (* | Pck_phase of clock_expr * rat *)
50
  (* | Pck_const of int * rat *)
51
  | Cvar (* of clock_set *) (* Monomorphic clock variable *)
52
  | Cunivar (* of clock_set *) (* Polymorphic clock variable *)
53 53
  | Clink of clock_expr (* During unification, make links instead of substitutions *)
54 54
  | Ccarrying of carrier_expr * clock_expr
55 55

  
56 56
type error =
57 57
  | Clock_clash of clock_expr * clock_expr
58
  | Not_pck
59
  | Clock_set_mismatch of clock_expr * clock_set
58
  (* | Not_pck *)
59
  (* | Clock_set_mismatch of clock_expr * clock_set *)
60 60
  | Cannot_be_polymorphic of clock_expr
61 61
  | Invalid_imported_clock of clock_expr
62 62
  | Invalid_const of clock_expr
......
66 66
  | Clock_extrusion of clock_expr * clock_expr
67 67

  
68 68
exception Unify of clock_expr * clock_expr
69
exception Subsume of clock_expr * clock_set
70 69
exception Mismatch of carrier_expr * carrier_expr
71 70
exception Scope_carrier of carrier_expr
72 71
exception Scope_clock of clock_expr
73 72
exception Error of Location.t * error
74 73

  
75
let print_ckset fmt s =
76
  match s with
77
  | CSet_all -> ()
78
  | CSet_pck (k,q) ->
79
      let (a,b) = simplify_rat q in
80
      if k = 1 && a = 0 then
81
        fprintf fmt "<:P"
82
      else
83
        fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
84

  
85 74
let rec print_carrier fmt cr =
86 75
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
87 76
  match cr.carrier_desc with
......
104 93
      (fprintf_list ~sep:" * " print_ck_long) cklist
105 94
  | Con (ck,c,l) ->
106 95
    fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
107
  | Pck_up (ck,k) ->
108
    fprintf fmt "%a*^%i" print_ck_long ck k
109
  | Pck_down (ck,k) ->
110
    fprintf fmt "%a/^%i" print_ck_long ck k
111
  | Pck_phase (ck,q) ->
112
    fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
113
  | Pck_const (n,p) ->
114
    fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
115
  | Cvar cset ->
116
    fprintf fmt "'_%i%a" ck.cid print_ckset cset
117
  | Cunivar cset ->
118
    fprintf fmt "'%i%a" ck.cid print_ckset cset
96
  | Cvar -> fprintf fmt "'_%i" ck.cid 
97
  | Cunivar -> fprintf fmt "'%i" ck.cid 
119 98
  | Clink ck' ->
120 99
    fprintf fmt "link %a" print_ck_long ck'
121 100
  | Ccarrying (cr,ck') ->
......
129 108
let new_ck desc scoped =
130 109
  incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
131 110

  
132
let new_var scoped =
133
  new_ck (Cvar CSet_all) scoped
111
let new_var scoped = new_ck Cvar scoped
134 112

  
135
let new_univar () =
136
  new_ck (Cunivar CSet_all) false
113
let new_univar () = new_ck Cunivar false
137 114

  
138 115
let new_carrier_id = ref (-1)
139 116

  
......
187 164

  
188 165
(* Removes all links in a clock. Only used for clocks
189 166
   simplification though. *)
190
let rec deep_repr ck =
167
let rec simplify ck =
191 168
  match ck.cdesc with
192 169
  | Carrow (ck1,ck2) ->
193
      new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped
170
      new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
194 171
  | Ctuple cl ->
195
      new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped
172
      new_ck (Ctuple (List.map simplify cl)) ck.cscoped
196 173
  | Con (ck', c, l) ->
197
      new_ck (Con (deep_repr ck', c, l)) ck.cscoped
198
  | Pck_up (ck',k) ->
199
      new_ck (Pck_up (deep_repr ck',k)) ck.cscoped
200
  | Pck_down (ck',k) ->
201
      new_ck (Pck_down (deep_repr ck',k)) ck.cscoped
202
  | Pck_phase (ck',q) ->
203
      new_ck (Pck_phase (deep_repr ck',q)) ck.cscoped
204
  | Pck_const (_,_) | Cvar _ | Cunivar _ -> ck
205
  | Clink ck' -> deep_repr ck'
206
  | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, deep_repr ck')) ck.cscoped
174
      new_ck (Con (simplify ck', c, l)) ck.cscoped
175
  | Cvar | Cunivar -> ck
176
  | Clink ck' -> simplify ck'
177
  | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, simplify ck')) ck.cscoped
207 178

  
208 179
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
209 180
    (ensured by language syntax) *)
......
233 204
let clock_of_impnode_clock ck =
234 205
  let ck = repr ck in
235 206
  match ck.cdesc with
236
  | Carrow _ | Clink _ | Cvar _ | Cunivar _ ->
207
  | Carrow _ | Clink _ | Cvar | Cunivar ->
237 208
      failwith "internal error clock_of_impnode_clock"
238 209
  | Ctuple cklist -> List.hd cklist
239
  | Con (_,_,_) | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_)
240
  | Pck_const (_,_) | Ccarrying (_,_) -> ck
241

  
242
(** [intersect set1 set2] returns the intersection of clock subsets
243
    [set1] and [set2]. *)
244
let intersect set1 set2 =
245
  match set1,set2 with
246
  | CSet_all,_ -> set2
247
  | _,CSet_all -> set1
248
  | CSet_pck (k,q), CSet_pck (k',q') ->
249
      let k'',q'' = lcm k k',max_rat q q' in
250
      CSet_pck (k'',q'')
251

  
252
(** [can_be_pck ck] returns true if [ck] "may be" a pclock (the uncertainty is
253
    due to clock variables) *)
254
let rec can_be_pck ck =
255
  match (repr ck).cdesc with
256
  | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) | Pck_const (_,_)
257
  | Cvar _ | Cunivar _ ->
258
      true
259
  | Ccarrying (_,ck') -> can_be_pck ck
260
  | _ -> false
261

  
262
(** [is_concrete_pck ck] returns true if [ck] is a concrete [pck] (pck
263
    transformations applied to a pck constant) *)
264
let rec is_concrete_pck ck =
265
  match ck.cdesc with
266
  | Carrow (_,_) | Ctuple _ | Con (_,_,_)
267
  | Cvar _ | Cunivar _ -> false
268
  | Pck_up (ck',_) | Pck_down (ck',_) -> is_concrete_pck ck'
269
  | Pck_phase (ck',_) -> is_concrete_pck ck'
270
  | Pck_const (_,_) -> true
271
  | Clink ck' -> is_concrete_pck ck'
272
  | Ccarrying (_,ck') -> false
210
  | Con (_,_,_) 
211
  | Ccarrying (_,_) -> ck
212

  
273 213

  
274 214
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
275 215
let rec is_polymorphic ck =
276 216
  match ck.cdesc with
277
  | Cvar _ | Pck_const (_,_) -> false
217
  | Cvar -> false
278 218
  | Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2)
279 219
  | Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl
280 220
  | Con (ck',_,_) -> is_polymorphic ck'
281
  | Pck_up (ck',_) | Pck_down (ck',_) -> is_polymorphic ck'
282
  | Pck_phase (ck',_) -> is_polymorphic ck'
283
  | Cunivar _ -> true
221
  | Cunivar  -> true
284 222
  | Clink ck' -> is_polymorphic ck'
285 223
  | Ccarrying (_,ck') -> is_polymorphic ck'
286 224

  
......
290 228
let rec constrained_vars_of_clock ck =
291 229
  let rec aux vars ck =
292 230
    match ck.cdesc with
293
    | Pck_const (_,_) ->
294
        vars
295
    | Cvar cset ->
296
        begin
297
          match cset with
298
          | CSet_all -> vars
299
          | _ ->
300
              list_union [ck] vars
301
        end
231
    | Cvar -> vars
302 232
    | Carrow (ck1,ck2) ->
303 233
        let l = aux vars ck1 in
304 234
        aux l ck2
......
307 237
          (fun acc ck' -> aux acc ck') 
308 238
          vars ckl
309 239
    | Con (ck',_,_) -> aux vars ck'
310
    | Pck_up (ck',_) | Pck_down (ck',_) -> aux vars ck'
311
    | Pck_phase (ck',_) -> aux vars ck'
312
    | Cunivar cset ->
313
        begin
314
          match cset with
315
          | CSet_all -> vars
316
          | _ -> list_union [ck] vars
317
        end
240
    | Cunivar -> vars
318 241
    | Clink ck' -> aux vars ck'
319 242
    | Ccarrying (_,ck') -> aux vars ck'
320 243
  in
321 244
  aux [] ck
322 245

  
323
(** [period ck] returns the period of [ck]. Expects a constant pclock
324
    expression belonging to the correct clock set. *)
325
let rec period ck =
326
  let rec aux ck =
327
    match ck.cdesc with
328
    | Carrow (_,_) | Ctuple _ | Con (_,_,_)
329
    | Cvar _ | Cunivar _ ->
330
        failwith "internal error: can only compute period of const pck"
331
    | Pck_up (ck',k) ->
332
        (aux ck')/.(float_of_int k)
333
    | Pck_down (ck',k) ->
334
        (float_of_int k)*.(aux ck')
335
    | Pck_phase (ck',_) ->
336
        aux ck'
337
    | Pck_const (n,_) ->
338
        float_of_int n
339
    | Clink ck' -> aux ck'
340
    | Ccarrying (_,ck') -> aux ck'
341
  in
342
  int_of_float (aux ck)
343

  
344
(** [phase ck] returns the phase of [ck]. It is not expressed as a
345
    fraction of the period, but instead as an amount of time. Expects a
346
    constant expression belonging to the correct P_k *)
347
let phase ck =
348
  let rec aux ck =
349
  match ck.cdesc with
350
  | Carrow (_,_) | Ctuple _ | Con (_,_,_)
351
  | Cvar _ | Cunivar _ ->
352
      failwith "internal error: can only compute phase of const pck"
353
  | Pck_up (ck',_) ->
354
      aux ck'
355
  | Pck_down (ck',k) ->
356
      aux ck'
357
  | Pck_phase (ck',(a,b)) ->
358
      let n = period ck' in
359
      let (a',b') = aux ck' in
360
      sum_rat (a',b') (n*a,b)
361
  | Pck_const (n,(a,b)) ->
362
      (n*a,b)
363
  | Clink ck' -> aux ck'
364
  | Ccarrying (_,ck') -> aux ck'
365
  in
366
  let (a,b) = aux ck in
367
  simplify_rat (a,b)
368

  
369 246
let eq_carrier cr1 cr2 =
370 247
  match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
371 248
 | Carry_const id1, Carry_const id2 -> id1 = id2
......
380 257
  match ck.cdesc with
381 258
  | Ctuple (ck'::_)
382 259
  | Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck'
383
  | Pck_up _ | Pck_down _ | Pck_phase _ | Pck_const _ | Cvar _ | Cunivar _ -> ck
260
  | Cvar | Cunivar -> ck
384 261
  | Carrow _ | Ctuple _ -> failwith "Internal error root"
385 262

  
386 263
(* Returns the branch of clock [ck] in its clock tree *)
......
419 296
let disjoint ck1 ck2 =
420 297
  eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
421 298

  
422
(** [normalize pck] returns the normal form of clock [pck]. *)
423
let normalize pck =
424
  let changed = ref true in
425
  let rec aux pck =
426
    match pck.cdesc with
427
    | Pck_up ({cdesc=Pck_up (pck',k')},k) ->
428
        changed:=true;
429
        new_ck (Pck_up (aux pck',k*k')) pck.cscoped
430
    | Pck_up ({cdesc=Pck_down (pck',k')},k) ->
431
        changed:=true;
432
        new_ck (Pck_down (new_ck (Pck_up (aux pck',k)) pck.cscoped,k')) pck.cscoped
433
    | Pck_up ({cdesc=Pck_phase (pck',(a,b))},k) ->
434
        changed:=true;
435
        new_ck (Pck_phase (new_ck (Pck_up (aux pck',k)) pck.cscoped,(a*k,b))) pck.cscoped
436
    | Pck_down ({cdesc=Pck_down (pck',k')},k) ->
437
        changed:=true;
438
        new_ck (Pck_down (aux pck',k*k')) pck.cscoped
439
    | Pck_down ({cdesc=Pck_phase (pck',(a,b))},k) ->
440
        changed:=true;
441
        new_ck (Pck_phase (new_ck (Pck_down (aux pck',k)) pck.cscoped,(a,b*k))) pck.cscoped
442
    | Pck_phase ({cdesc=Pck_phase (pck',(a',b'))},(a,b)) ->
443
        changed:=true;
444
        let (a'',b'') = sum_rat (a,b) (a',b') in
445
        new_ck (Pck_phase (aux pck',(a'',b''))) pck.cscoped
446
    | Pck_up (pck',k') ->
447
        new_ck (Pck_up (aux pck',k')) pck.cscoped
448
    | Pck_down (pck',k') ->
449
        new_ck (Pck_down (aux pck',k')) pck.cscoped
450
    | Pck_phase (pck',k') ->
451
        new_ck (Pck_phase (aux pck',k')) pck.cscoped
452
    | Ccarrying (cr,ck') ->
453
        new_ck (Ccarrying (cr, aux ck')) pck.cscoped
454
    | _ -> pck
455
  in
456
  let nf=ref pck in
457
  while !changed do
458
    changed:=false;
459
    nf:=aux !nf
460
  done;
461
  !nf
462

  
463
(** [canonize pck] reduces transformations of [pck] and removes
464
    identity transformations. Expects a normalized periodic clock ! *)
465
let canonize pck =
466
  let rec remove_id_trans pck =
467
    match pck.cdesc with
468
    | Pck_up (pck',1) | Pck_down (pck',1) | Pck_phase (pck',(0,_)) ->
469
        remove_id_trans pck'
470
    | _ -> pck
471
  in
472
  let pck =
473
    match pck.cdesc with
474
    | Pck_phase ({cdesc=Pck_down ({cdesc=Pck_up (v,k)},k')},k'') ->
475
        let gcd = gcd k k' in
476
        new_ck (Pck_phase
477
                  (new_ck (Pck_down
478
                             (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd))
479
                     pck.cscoped,k''))
480
          pck.cscoped
481
    | Pck_down ({cdesc=Pck_up (v,k)},k') ->
482
        let gcd = gcd k k' in
483
        new_ck (Pck_down (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) pck.cscoped
484
    | _ -> pck
485
  in
486
  remove_id_trans pck
487

  
488
(** [simplify pck] applies pclocks simplifications to [pck] *)
489
let simplify pck =
490
  if (is_concrete_pck pck) then
491
    let n = period pck in
492
    let (a,b) = phase pck in
493
    let phase' = simplify_rat (a,b*n) in 
494
    new_ck (Pck_const (n,phase')) pck.cscoped
495
  else
496
    let pck' = deep_repr pck in
497
    let nf_pck = normalize pck' in
498
    canonize nf_pck
499
        
500 299
let print_cvar fmt cvar =
501 300
  match cvar.cdesc with
502
  | Cvar cset ->
301
  | Cvar ->
503 302
 (*
504 303
      if cvar.cscoped
505 304
      then
506
	fprintf fmt "[_%s%a]"
305
	fprintf fmt "[_%s]"
507 306
	  (name_of_type cvar.cid)
508
	  print_ckset cset
509 307
      else
510 308
 *)
511
	fprintf fmt "_%s%a"
309
	fprintf fmt "_%s"
512 310
	  (name_of_type cvar.cid)
513
	  print_ckset cset
514
  | Cunivar cset ->
311
  | Cunivar ->
515 312
 (*
516 313
      if cvar.cscoped
517 314
      then
518
	fprintf fmt "['%s%a]"
315
	fprintf fmt "['%s]"
519 316
	  (name_of_type cvar.cid)
520
	  print_ckset cset
521 317
      else
522 318
 *)
523
	fprintf fmt "'%s%a"
319
	fprintf fmt "'%s"
524 320
	  (name_of_type cvar.cid)
525
	  print_ckset cset
526 321
  | _ -> failwith "Internal error print_cvar"
527 322

  
528 323
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
529 324
   complexity. *)
530 325
let print_ck fmt ck =
531 326
  let rec aux fmt ck =
532
    let ck = simplify ck in
533 327
    match ck.cdesc with
534 328
    | Carrow (ck1,ck2) ->
535 329
      fprintf fmt "%a -> %a" aux ck1 aux ck2
......
538 332
	(fprintf_list ~sep:" * " aux) cklist
539 333
    | Con (ck,c,l) ->
540 334
      fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
541
    | Pck_up (ck,k) ->
542
      fprintf fmt "%a*.%i" aux ck k
543
    | Pck_down (ck,k) ->
544
      fprintf fmt "%a/.%i" aux ck k
545
    | Pck_phase (ck,q) ->
546
      fprintf fmt "%a->.%a" aux ck print_rat (simplify_rat q)
547
    | Pck_const (n,p) ->
548
      fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
549
    | Cvar cset ->
335
    | Cvar ->
550 336
(*
551 337
      if ck.cscoped
552 338
      then
......
554 340
      else
555 341
*)
556 342
	fprintf fmt "_%s" (name_of_type ck.cid)
557
    | Cunivar cset ->
343
    | Cunivar ->
558 344
(*
559 345
      if ck.cscoped
560 346
      then
......
575 361

  
576 362
(* prints only the Con components of a clock, useful for printing nodes *)
577 363
let rec print_ck_suffix fmt ck =
578
  let ck = simplify ck in
579 364
  match ck.cdesc with
580 365
  | Carrow _
581 366
  | Ctuple _
582
  | Cvar _
583
  | Cunivar _   -> ()
367
  | Cvar 
368
  | Cunivar    -> ()
584 369
  | Con (ck,c,l) ->
585 370
    fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
586 371
  | Clink ck' ->
587 372
    print_ck_suffix fmt ck'
588 373
  | Ccarrying (cr,ck') ->
589 374
    fprintf fmt "%a" print_ck_suffix ck'
590
  | _ -> assert false
375

  
591 376

  
592 377
let pp_error fmt = function
593 378
  | Clock_clash (ck1,ck2) ->
......
595 380
      fprintf fmt "Expected clock %a, got clock %a@."
596 381
      print_ck ck1
597 382
      print_ck ck2
598
  | Not_pck ->
599
    fprintf fmt "The clock of this expression must be periodic@."
600 383
  | Carrier_mismatch (cr1, cr2) ->
601 384
     fprintf fmt "Name clash. Expected clock %a, got clock %a@."
602 385
       print_carrier cr1
603 386
       print_carrier cr2
604
  | Clock_set_mismatch (ck,cset) ->
605
      reset_names ();
606
    fprintf fmt "Clock %a is not included in clock set %a@."
607
      print_ck ck
608
      print_ckset cset
609 387
  | Cannot_be_polymorphic ck ->
610 388
      reset_names ();
611 389
    fprintf fmt "The main node cannot have a polymorphic clock: %a@."
......
630 408
      print_ck ck
631 409

  
632 410
let const_of_carrier cr =
633
 match (carrier_repr cr).carrier_desc with
634
 | Carry_const id -> id
635
 | Carry_name
636
 | Carry_var
637
 | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
411
  match (carrier_repr cr).carrier_desc with
412
  | Carry_const id -> id
413
  | Carry_name
414
  | Carry_var
415
  | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
638 416
 
639 417
let uneval const cr =
640 418
  (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
src/inliner.ml
39 39
    eq_lhs = List.map rename eq.eq_lhs; 
40 40
    eq_rhs = rename_expr rename eq.eq_rhs
41 41
  }
42

  
43
let rec add_expr_reset_cond cond expr =
44
  let aux = add_expr_reset_cond cond in
45
  let new_desc = 
46
    match expr.expr_desc with
47
    | Expr_const _
48
    | Expr_ident _ -> expr.expr_desc
49
    | Expr_tuple el -> Expr_tuple (List.map aux el)
50
    | Expr_ite (c, t, e) -> Expr_ite (aux c, aux t, aux e)
51
      
52
    | Expr_arrow (e1, e2) -> 
53
      (* we replace the expression e1 -> e2 by e1 -> (if cond then e1 else e2) *)
54
      let e1 = aux e1 and e2 = aux e2 in
55
      (* inlining is performed before typing. we can leave the fields free *)
56
      let new_e2 = mkexpr expr.expr_loc (Expr_ite (cond, e1, e2)) in
57
      Expr_arrow (e1, new_e2) 
58

  
59
    | Expr_fby _ -> assert false (* TODO: deal with fby. This hasn't been much handled yet *)
60

  
61
    | Expr_array el -> Expr_array (List.map aux el)
62
    | Expr_access (e, dim) -> Expr_access (aux e, dim)
63
    | Expr_power (e, dim) -> Expr_power (aux e, dim)
64
    | Expr_pre e -> Expr_pre (aux e)
65
    | Expr_when (e, id, l) -> Expr_when (aux e, id, l)
66
    | Expr_merge (id, cases) -> Expr_merge (id, List.map (fun (l,e) -> l, aux e) cases)
67

  
68
    | Expr_appl (id, args, reset_opt) -> 
69
      (* we "add" cond to the reset field. *)
70
      let new_reset = match reset_opt with
71
	  None -> cond
72
	| Some cond' -> mkpredef_call cond'.expr_loc "||" [cond; cond']
73
      in
74
      Expr_appl (id, args, Some new_reset)
75
      
76

  
77
  in
78
  { expr with expr_desc = new_desc }
79

  
80
let add_eq_reset_cond cond eq =
81
  { eq with eq_rhs = add_expr_reset_cond cond eq.eq_rhs }
42 82
(*
43 83
let get_static_inputs input_arg_list =
44 84
 List.fold_right (fun (vdecl, arg) res ->
......
54 94
   else res)
55 95
   input_arg_list []
56 96
*)
97

  
98

  
57 99
(* 
58 100
    expr, locals', eqs = inline_call id args' reset locals node nodes
59 101

  
......
64 106
the resulting expression is tuple_of_renamed_outputs
65 107
   
66 108
TODO: convert the specification/annotation/assert and inject them
67
DONE: annotations
68
TODO: deal with reset
69 109
*)
70
let inline_call node orig_expr args reset locals caller =
71
  let loc = orig_expr.expr_loc in
72
  let uid = orig_expr.expr_tag in
110
(** [inline_call node loc uid args reset locals caller] returns a tuple (expr,
111
    locals, eqs, asserts)    
112
*)
113
let inline_call node loc uid args reset locals caller =
73 114
  let rename v =
74 115
    if v = tag_true || v = tag_false || not (is_node_var node v) then v else
75 116
      Corelang.mk_new_node_name caller (Format.sprintf "%s_%i_%s" node.node_id uid v)
......
97 138
	 v.var_dec_const,
98 139
	 Utils.option_map (rename_expr rename) v.var_dec_value) in
99 140
    begin
100
(*
101
      (try
102
	 Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
103
	 Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
104
       with Not_found -> ());
105
      (try
106
Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
107
       with Not_found -> ());
108
(*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
109
*)
141
      (*
142
	(try
143
	Format.eprintf "Inliner.inline_call unify %a %a@." Types.print_ty vdecl.var_type Dimension.pp_dimension (List.assoc v.var_id static_inputs);
144
	Typing.unify vdecl.var_type (Type_predef.type_static (List.assoc v.var_id static_inputs) (Types.new_var ()))
145
	with Not_found -> ());
146
	(try
147
	Clock_calculus.unify vdecl.var_clock (Clock_predef.ck_carrier (List.assoc v.var_id carrier_inputs) (Clocks.new_var true))
148
	with Not_found -> ());
149
      (*Format.eprintf "Inliner.inline_call res=%a@." Printers.pp_var vdecl;*)
150
      *)
110 151
      vdecl
111 152
    end
112
    (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
153
  (*Format.eprintf "Inliner.rename_var %a@." Printers.pp_var v;*)
113 154
  in
114 155
  let inputs' = List.map (fun (vdecl, _) -> rename_var vdecl) dynamic_inputs in
115 156
  let outputs' = List.map rename_var node.node_outputs in
116 157
  let locals' =
117
      (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
158
    (List.map (fun (vdecl, arg) -> let vdecl' = rename_var vdecl in { vdecl' with var_dec_value = Some (Corelang.expr_of_dimension arg) }) static_inputs)
118 159
    @ (List.map rename_var node.node_locals) 
119
in
160
  in
120 161
  (* checking we are at the appropriate (early) step: node_checks and
121 162
     node_gencalls should be empty (not yet assigned) *)
122 163
  assert (node.node_checks = []);
123 164
  assert (node.node_gencalls = []);
124 165

  
125
  (* Bug included: todo deal with reset *)
126
  assert (reset = None);
127

  
128
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs', expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
166
  (* Expressing reset locally in equations *)
167
  let eqs_r' =
168
    match reset with
169
      None -> eqs'
170
    | Some cond -> List.map (add_eq_reset_cond cond) eqs'
171
  in
172
  let assign_inputs = mkeq loc (List.map (fun v -> v.var_id) inputs',
173
                                expr_of_expr_list args.expr_loc (List.map snd dynamic_inputs)) in
129 174
  let expr = expr_of_expr_list loc (List.map expr_of_vdecl outputs')
130 175
  in
131 176
  let asserts' = (* We rename variables in assert expressions *)
......
134 179
	{a with assert_expr = 
135 180
	    let expr = a.assert_expr in
136 181
	    rename_expr rename expr
137
      })
182
	})
138 183
      node.node_asserts 
139 184
  in
140 185
  let annots' =
......
142 187
  in
143 188
  expr, 
144 189
  inputs'@outputs'@locals'@locals, 
145
  assign_inputs::eqs',
190
  assign_inputs::eqs_r',
146 191
  asserts',
147 192
  annots'
148 193

  
......
194 239
      let called = node_of_top called in
195 240
      let called' = inline_node called nodes in
196 241
      let expr, locals', eqs'', asserts'', annots'' = 
197
	inline_call called' expr args' reset locals' node in
242
	inline_call called' expr.expr_loc expr.expr_tag args' reset locals' node in
198 243
      expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
199 244
    else 
200 245
      (* let _ =     Format.eprintf "Not inlining call to %s@." id in *)
src/lustreSpec.ml
46 46
and clock_dec_desc =
47 47
  | Ckdec_any
48 48
  | Ckdec_bool of (ident * ident) list 
49
  | Ckdec_pclock of int * rat
49

  
50 50

  
51 51
type constant =
52 52
  | Const_int of int
......
241 241
  | MLocalAssign of var_decl * value_t
242 242
  | MStateAssign of var_decl * value_t
243 243
  | MReset of ident
244
  | MNoReset of ident
244 245
  | MStep of var_decl list * ident * value_t list
245 246
  | MBranch of value_t * (label * instr_t list) list
246 247
  | MComment of string
src/machine_code.ml
36 36
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
37 37
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
38 38
    | MReset i           -> Format.fprintf fmt "reset %s" i
39
    | MNoReset i         -> Format.fprintf fmt "noreset %s" i
39 40
    | MStep (il, i, vl)  ->
40 41
      Format.fprintf fmt "%a = %s (%a)"
41 42
	(Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
......
135 136
    var_dec_const = false;
136 137
    var_dec_value = None;
137 138
    var_type =  typ;
138
    var_clock = Clocks.new_ck (Clocks.Cvar Clocks.CSet_all) true;
139
    var_clock = Clocks.new_ck Clocks.Cvar true;
139 140
    var_loc = Location.dummy_loc
140 141
  }
141 142

  
......
352 353
    | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
353 354
      let nd = node_from_name id in
354 355
      Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
355
    | Expr_ite (g,t,e) -> (
356
    (*| Expr_ite (g,t,e) -> (
356 357
      (* special treatment depending on the active backend. For horn backend, ite
357 358
	 are preserved in expression. While they are removed for C or Java
358 359
	 backends. *)
......
360 361
	Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
361 362
      | "C" | "java" | _ -> 
362 363
	(Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
363
    )
364
    )*)
364 365
    | _                   -> raise NormalizationError
365 366
  in
366 367
  mk_val value_desc expr.expr_type
......
373 374
let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
374 375
  match expr.expr_desc with
375 376
  | Expr_ite   (c, t, e) -> let g = translate_guard node args c in
376
			    conditional g [translate_act node args (y, t)]
377
			    conditional g
378
                              [translate_act node args (y, t)]
377 379
                              [translate_act node args (y, e)]
378
  | Expr_merge (x, hl)   -> MBranch (translate_ident node args x, List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
380
  | Expr_merge (x, hl)   -> MBranch (translate_ident node args x,
381
                                     List.map (fun (t,  h) -> t, [translate_act node args (y, h)]) hl)
379 382
  | _                    -> MLocalAssign (y, translate_expr node args expr)
380 383

  
381 384
let reset_instance node args i r c =
382 385
  match r with
383 386
  | None        -> []
384 387
  | Some r      -> let g = translate_guard node args r in
385
                   [control_on_clock node args c (conditional g [MReset i] [])]
388
                   [control_on_clock node args c (conditional g [MReset i] [MNoReset i])]
386 389

  
387 390
let translate_eq node ((m, si, j, d, s) as args) eq =
388 391
  (* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
......
434 437
      then []
435 438
      else reset_instance node args o r call_ck) @
436 439
       (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
437

  
440
(*
438 441
   (* special treatment depending on the active backend. For horn backend, x = ite (g,t,e)
439 442
      are preserved. While they are replaced as if g then x = t else x = e in  C or Java
440 443
      backends. *)
......
450 453
	(MLocalAssign (var_x, translate_expr node args eq.eq_rhs))::s)
451 454
    )
452 455

  
456
*)
453 457
  | [x], _                                       -> (
454 458
    let var_x = get_node_var x node in
455 459
    (m, si, j, d,
......
556 560
	(* special treatment depending on the active backend. For horn backend,
557 561
	   common branches are not merged while they are in C or Java
558 562
	   backends. *)
559
	match !Options.output with
563
	(*match !Options.output with
560 564
	| "horn" -> s
561
	| "C" | "java" | _ -> join_guards_list s
565
	| "C" | "java" | _ ->*) join_guards_list s
562 566
      );
563 567
      step_asserts =
564 568
	let exprl = List.map (fun assert_ -> assert_.assert_expr ) nd.node_asserts in
src/main_lustre_compiler.ml
88 88
  end
89 89

  
90 90

  
91
let functional_backend () = 
92
  match !Options.output with
93
  | "horn" | "lustre" | "acsl" -> true
94
  | _ -> false
95

  
91 96
(* From prog to prog *)
92 97
let stage1 prog dirname basename =
93 98
  (* Removing automata *) 
......
122 127

  
123 128
  (* Typing *)
124 129
  let computed_types_env = type_decls type_env prog in
125
  
130

  
126 131
  (* Clock calculus *)
127 132
  let computed_clocks_env = clock_decls clock_env prog in
128 133

  
......
148 153
  in
149 154
  *)
150 155
  (* Delay calculus *)
151
  (*
156
  (* TO BE DONE LATER (Xavier)
152 157
    if(!Options.delay_calculus)
153 158
    then
154 159
    begin
......
213 218
      end
214 219
    else
215 220
      begin
216
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping FP numbers@,");
221
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping floating-point numbers@,");
217 222
	prog
218 223
      end in
219 224
  Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
......
221 226
  (* Checking array accesses *)
222 227
  if !Options.check then
223 228
    begin
224
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,");
229
      Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking array accesses@,");
225 230
      Access.check_prog prog;
226 231
    end;
227 232

  
......
257 262
  let machine_code =
258 263
    if !Options.optimization >= 4 && !Options.output <> "horn" then
259 264
      begin
260
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 3)@,");
265
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: common sub-expression elimination@,");
261 266
	Optimize_machine.machines_cse machine_code
262 267
      end
263 268
    else
......
267 272
  let machine_code, removed_table = 
268 273
    if !Options.optimization >= 2 && !Options.output <> "horn" then
269 274
      begin
270
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@ ");
275
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: constants inlining@,");
271 276
	Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
272 277
      end
273 278
    else
......
277 282
  let machine_code = 
278 283
    if !Options.optimization >= 3 && !Options.output <> "horn" then
279 284
      begin
280
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@ ");
285
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization: minimize stack usage by reusing variables@,");
281 286
	let node_schs    = Scheduling.remove_prog_inlined_locals removed_table node_schs in
282 287
	let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
283 288
	Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
......
292 297
    if !Options.salsa_enabled then
293 298
      begin
294 299
	check_main ();
295
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization (phase 3)@ ");
300
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization: optimizing floating-point accuracy with Salsa@,");
296 301
	(* Selecting float constants for Salsa *)
297 302
	let constEnv = List.fold_left (
298 303
	  fun accu c_topdecl ->
......
348 353
	let source_out = open_out source_file in
349 354
	let fmt = formatter_of_out_channel source_out in
350 355
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
351
        Horn_backend.translate fmt basename prog machine_code;
356
        Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
352 357
	(* Tracability file if option is activated *)
353 358
	if !Options.traces then (
354
	let traces_file = destname ^ ".traces" in (* Could be changed *)
359
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
355 360
	let traces_out = open_out traces_file in
356 361
	let fmt = formatter_of_out_channel traces_out in
357 362
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
358
	Horn_backend.traces_file fmt basename prog machine_code;
363
	Horn_backend_traces.traces_file fmt basename prog machine_code;
359 364
	)
360 365
      end
361 366
    | "lustre" ->
src/normalization.ml
393 393
	  annots = List.map (fun v ->
394 394
	    let eq =
395 395
	      try
396
		List.find (fun eq -> eq.eq_lhs = [v.var_id]) (defs@assert_defs) 
397
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
396
		List.find (fun eq -> List.exists (fun v' -> v' = v.var_id ) eq.eq_lhs) (defs@assert_defs) 
397
	      with Not_found -> 
398
		(
399
		  Format.eprintf "Traceability annotation generation: var %s not found@." v.var_id; 
400
		  assert false
401
		) 
402
	    in
398 403
	    let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
399 404
	    let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
400 405
	    (["traceability"], pair)
src/optimize_machine.ml
31 31
  | MLocalAssign (i,v) -> MLocalAssign (i, e_expr v)
32 32
  | MStateAssign (i,v) -> MStateAssign (i, e_expr v)
33 33
  | MReset i           -> instr
34
  | MNoReset i         -> instr
34 35
  | MStep (il, i, vl)  -> MStep(il, i, List.map e_expr vl)
35 36
  | MBranch (g,hl)     -> 
36 37
    MBranch
......
51 52
  | Cst _ | StateVar _ -> expr
52 53

  
53 54
let eliminate_dim elim dim =
54
  Dimension.expr_replace_expr (fun v -> try dimension_of_value (IMap.find v elim) with Not_found -> mkdim_ident dim.dim_loc v) dim
55
  Dimension.expr_replace_expr 
56
    (fun v -> try
57
		dimension_of_value (IMap.find v elim) 
58
      with Not_found -> mkdim_ident dim.dim_loc v) 
59
    dim
55 60

  
56 61
let unfold_expr_offset m offset expr =
57 62
  List.fold_left
......
100 105
  | MLocalAssign (v, expr) -> MLocalAssign (v, simplify_expr_offset m expr)
101 106
  | MStateAssign (v, expr) -> MStateAssign (v, simplify_expr_offset m expr)
102 107
  | MReset id              -> instr
108
  | MNoReset id            -> instr
103 109
  | MStep (outputs, id, inputs) -> MStep (outputs, id, List.map (simplify_expr_offset m) inputs)
104 110
  | MBranch (cond, brl)
105 111
    -> MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
src/parse.ml
32 32
  | Undefined_token tok   -> fprintf fmt "undefined token '%s'" tok
33 33
  | Unfinished_string        -> fprintf fmt "unfinished string"
34 34
  | Unfinished_comment  -> fprintf fmt "unfinished comment"
35
  | Syntax_error               -> fprintf fmt "syntax error"
35
  | Syntax_error               -> fprintf fmt ""
36 36
  | Unfinished_annot        -> fprintf fmt "unfinished annotation"
37 37
  | Unfinished_node_spec -> fprintf fmt "unfinished node specification"
38 38
  | Annot_error s              -> fprintf fmt "impossible to parse the following annotation:@.%s@.@?" s
src/parser_lustre.mly
623 623

  
624 624
ident_list:
625 625
  vdecl_ident {[$1]}
626
| ident_list COMMA vdecl_ident {$3::$1}
626
| vdecl_ident COMMA ident_list {$1::$3}
627 627

  
628 628
SCOL_opt:
629 629
    SCOL {} | {}
src/typing.ml
542 542
   in environment [env] *)
543 543
let type_coreclock env ck id loc =
544 544
  match ck.ck_dec_desc with
545
  | Ckdec_any | Ckdec_pclock (_,_) -> ()
545
  | Ckdec_any -> ()
546 546
  | Ckdec_bool cl ->
547 547
      let dummy_id_expr = expr_of_ident id loc in
548 548
      let when_expr =

Also available in: Unified diff