Project

General

Profile

Revision 8f1c7e91 src/clock_calculus.ml

View differences:

src/clock_calculus.ml
251 251
          cr1.carrier_desc <- Carry_link cr2;
252 252
          update_scope_carrier cr1.carrier_scoped cr2
253 253
        end
254
    | _,_ -> (assert false)
254
    | _,_ -> assert false
255

  
256
(* Semi-unifies two clock carriers *)
257
let semi_unify_carrier cr1 cr2 =
258
  let cr1 = carrier_repr cr1 in
259
  let cr2 = carrier_repr cr2 in
260
  if cr1=cr2 then ()
261
  else
262
    match cr1.carrier_desc, cr2.carrier_desc with
263
    | Carry_const id1, Carry_const id2 ->
264
      if id1 <> id2 then raise (Mismatch (cr1, cr2))
265
    | Carry_const _, Carry_name ->
266
      begin
267
	cr2.carrier_desc <- Carry_link cr1;
268
	update_scope_carrier cr2.carrier_scoped cr1
269
      end
270
    | Carry_name, Carry_const _ -> raise (Mismatch (cr1, cr2))
271
    | Carry_name, Carry_name ->
272
      if cr1.carrier_id < cr2.carrier_id then
273
        begin
274
          cr2.carrier_desc <- Carry_link cr1;
275
          update_scope_carrier cr2.carrier_scoped cr1
276
        end
277
      else
278
        begin
279
          cr1.carrier_desc <- Carry_link cr2;
280
          update_scope_carrier cr1.carrier_scoped cr2
281
        end
282
    | _,_ -> assert false
255 283

  
256 284
(** [unify ck1 ck2] unifies clocks [ck1] and [ck2]. Raises [Unify
257 285
    (ck1,ck2)] if the clocks are not unifiable.*)
......
355 383
          subsume ck2 (CSet_pck (b,(a,b)));
356 384
          let ck2' = simplify (new_ck (Pck_phase (ck2,(-a,b))) true) in
357 385
          unify pck1' ck2'
358
      (* Corner case for some functions like ite, need to unify guard clock
359
	 with output clocks *)
360
(*
361
      | Ctuple ckl, (Cvar _) -> List.iter (unify ck2) ckl
362
      | (Cvar _), Ctuple ckl ->	List.iter (unify ck1) ckl
363
*)
386
      | Cunivar _, _ | _, Cunivar _ -> ()
387
      | _,_ -> raise (Unify (ck1,ck2))
388

  
389
(** [unify ck1 ck2] semi-unifies clocks [ck1] and [ck2]. Raises [Unify
390
    (ck1,ck2)] if the clocks are not semi-unifiable.*)
391
let rec semi_unify ck1 ck2 =
392
  let ck1 = repr ck1 in
393
  let ck2 = repr ck2 in
394
  if ck1=ck2 then
395
    ()
396
  else
397
      match ck1.cdesc,ck2.cdesc with
398
      | Cvar cset1,Cvar cset2->
399
          if ck1.cid < ck2.cid then
400
            begin
401
              ck2.cdesc <- Clink (simplify ck1);
402
              update_scope ck2.cscoped ck1
403
            end
404
          else
405
            begin
406
              ck1.cdesc <- Clink (simplify ck2);
407
              update_scope ck1.cscoped ck2
408
            end
409
      | (Cvar cset,_) -> raise (Unify (ck1,ck2))
410
      | (_, (Cvar cset)) when (not (occurs ck2 ck1)) ->
411
          update_scope ck2.cscoped ck1;
412
          ck2.cdesc <- Clink (simplify ck1)
413
      | Ccarrying (cr1,ck1'),Ccarrying (cr2,ck2') ->
414
          semi_unify_carrier cr1 cr2;
415
          semi_unify ck1' ck2'
416
      | Ccarrying (_,_),_ | _,Ccarrying (_,_) ->
417
          raise (Unify (ck1,ck2))
418
      | Carrow (c1,c2), Carrow (c1',c2') ->
419
	begin
420
          semi_unify c1 c1';
421
	  semi_unify c2 c2'
422
	end
423
      | Ctuple ckl1, Ctuple ckl2 ->
424
          if (List.length ckl1) <> (List.length ckl2) then
425
            raise (Unify (ck1,ck2));
426
          List.iter2 semi_unify ckl1 ckl2
427
      | Con (ck',c1,l1), Con (ck'',c2,l2) when l1=l2 ->
428
          semi_unify_carrier c1 c2;
429
          semi_unify ck' ck''
364 430
      | Cunivar _, _ | _, Cunivar _ -> ()
365 431
      | _,_ -> raise (Unify (ck1,ck2))
366 432

  
......
442 508
  | Mismatch (cr1,cr2) ->
443 509
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
444 510

  
511
let try_semi_unify ck1 ck2 loc =
512
  try
513
    semi_unify ck1 ck2
514
  with
515
  | Unify (ck1',ck2') ->
516
    raise (Error (loc, Clock_clash (ck1',ck2')))
517
  | Subsume (ck,cset) ->
518
    raise (Error (loc, Clock_set_mismatch (ck,cset)))
519
  | Mismatch (cr1,cr2) ->
520
    raise (Error (loc, Carrier_mismatch (cr1,cr2)))
521

  
445 522
(* Checks whether ck1 is a subtype of ck2 *)
446 523
let rec clock_subtyping ck1 ck2 =
447 524
  match (repr ck1).cdesc, (repr ck2).cdesc with
......
775 852
let clock_prog env decls =
776 853
  List.fold_left (fun e decl -> clock_top_decl e decl) env decls
777 854

  
855
(* Once the Lustre program is fully clocked,
856
   we must get back to the original description of clocks,
857
   with constant parameters, instead of unifiable internal variables. *)
858

  
859
(* The following functions aims at 'unevaluating' carriers occuring in clock expressions,
860
   i.e. replacing unifiable second_order variables with the original carrier names.
861
   Once restored in this formulation, clocks may be meaningfully printed.
862
*)
863
let uneval_vdecl_generics vdecl =
864
 if Types.is_clock_type vdecl.var_type
865
 then
866
   match get_carrier_name vdecl.var_clock with
867
   | None    -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false)
868
   | Some cr -> Clocks.uneval vdecl.var_id cr
869

  
870
let uneval_node_generics vdecls =
871
  List.iter uneval_vdecl_generics vdecls
872

  
873
let uneval_top_generics decl =
874
  match decl.top_decl_desc with
875
  | Node nd ->
876
      uneval_node_generics (nd.node_inputs @ nd.node_outputs)
877
  | ImportedNode nd ->
878
      uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
879
  | ImportedFun nd ->
880
      ()
881
  | Consts clist -> ()
882
  | Open _  -> ()
883

  
884
let uneval_prog_generics prog =
885
 List.iter uneval_top_generics prog
886

  
778 887
let check_env_compat header declared computed =
888
  uneval_prog_generics header;
779 889
  Env.iter declared (fun k decl_clock_k -> 
780 890
    let computed_c = instantiate (ref []) (ref []) (Env.lookup_value computed k) in
781
    try_unify decl_clock_k computed_c Location.dummy_loc
891
    try_semi_unify decl_clock_k computed_c Location.dummy_loc
782 892
  ) 
783 893
(* Local Variables: *)
784 894
(* compile-command:"make -C .." *)

Also available in: Unified diff