Newer
Older
(** Time-stamp: <modified the 26/05/2009 (at 17:02) by Erwan Jahier> *)
open Printf
open Lxm
open Errors
let ci2str = LicDump.string_of_clock2
(* exported *)
type subst1 = (Ident.t * Ident.t) list
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
(**
A dedicated kind of substitution tailored to deal with clock variables
(Eff.ClockVar). A few fact motivating why a general unification algorithm
is not necessary.
- ClockVar can only be created at val_exp leaves.
- each leave returns a unique ClockVar
- By construction, clocks of the form "On(id,clk)" do not
contain ClockVar (I should probably craft a new Eff.clock type
that materialize this fact).
- When unifying two Eff.clocks, as far as ClockVar are concerned, there is
therefore only two cases:
(1) c1,c2= ClockVar i, ClockVar j
(2) c1,c2= ClockVar i, clk (where clk does not contain ClockVar _ )
We do that by constructing subst2 only via the function [add_link2] (case 1) and
[add_subst2] (case 2).
And since [add_subst2] is linear (cf the code), this unification algorithm
is also linear.
*)
module IntMap = Map.Make(struct type t = int let compare = compare end)
module IntSet = Set.Make(struct type t = int let compare = compare end)
(* Clock variable information associated to a clock var cv *)
type cv_info =
| Equiv of IntSet.t (* the list of CV that are equals to cv *)
| Clk of clock (* a ground clock *)
(* The idea of this DS is the following. We maintain, for free CVs,
the list of CVs that are equals to them. Hence, once a CV is
becomes bounded, it is easy to bound all the CVs that were equal to
it.
*)
type cv_tbl = cv_info IntMap.t
type subst2 = { cpt : int; cv_tbl : cv_tbl }
type subst = subst1 * subst2
(******************************************************************************)
let (subst2_to_string : subst2 -> string) =
fun s2 ->
(String.concat ",\n\t "
(IntMap.fold
(fun i cvi acc ->
(match cvi with
| Clk c ->
"CV_" ^ (string_of_int i) ^ "/" ^
(ci2str c)
| Equiv is -> "CV_" ^ (string_of_int i) ^ " in {" ^
(String.concat ","
(IntSet.fold (fun i acc -> (string_of_int i)::acc) is [])) ^
"}"
)::acc
)
s2.cv_tbl
[]
)) ^ "\n"
let (subst_to_string : subst -> string) =
fun (s1,s2) ->
let v2s = Ident.to_string in
(String.concat ", " (List.map (fun (v1,v2) -> (v2s v1) ^ "/" ^ (v2s v2)) s1)) ^
"\nsubst2:\n\t " ^ (subst2_to_string s2)
(******************************************************************************)
let (empty_subst2:subst2) = { cpt = 0 ; cv_tbl = IntMap.empty }
let (empty_subst:subst) = [], empty_subst2
let (add_subst1 : Ident.t -> Ident.t -> subst1 -> subst1) =
fun id1 id2 s ->
if List.mem_assoc id1 s then s else (id1,id2)::s
let rec (add_link2 : int -> int -> subst2 -> subst2) =
fun i j s2 ->
if j > i then add_link2 j i s2 else
let tbl = s2.cv_tbl in
let cvi_i = IntMap.find i tbl
and cvi_j = IntMap.find j tbl in
let tbl =
match cvi_i, cvi_j with
| Equiv li, Equiv lj ->
let l = IntSet.union li lj in
let tbl = IntSet.fold (fun i tbl -> IntMap.add i (Equiv l) tbl) l tbl in
tbl
| Equiv l, Clk c
| Clk c, Equiv l ->
IntSet.fold (fun i tbl -> IntMap.add i (Clk c) tbl) l tbl
| Clk c1, Clk c2 ->
assert (c1=c2); tbl
in
{ s2 with cv_tbl = tbl }
let (add_subst2 : int -> Eff.clock -> subst2 -> subst2) =
fun i c s2 ->
let tbl =
match IntMap.find i s2.cv_tbl with
| Equiv l ->
IntSet.fold (fun i tbl -> IntMap.add i (Clk c) tbl) l s2.cv_tbl
| Clk c2 ->
IntMap.add i (Clk c2) s2.cv_tbl
in
{ s2 with cv_tbl = tbl }
let (find_subst1 : Ident.t -> subst1 -> Ident.t option) =
fun id s ->
try Some (List.assoc id s) with Not_found -> None
let (find_subst2 : int -> subst2 -> Eff.clock option) =
fun i s2 ->
try
match IntMap.find i s2.cv_tbl with
| Equiv l -> None
| Clk c -> Some c
with Not_found ->
print_string (" *** Don't know anything about CV" ^ (string_of_int i) ^ "\n");
print_string (" in the table : " ^ subst2_to_string s2);
flush stdout;
assert false
(******************************************************************************)
(* Stuff to generate fresh clock vars *)
(* exported *)
let (new_clock_var : subst -> subst * Eff.clock) =
fun (s1, s2) ->
let clk = ClockVar s2.cpt in
let tbl = IntMap.add s2.cpt (Equiv (IntSet.singleton s2.cpt)) s2.cv_tbl in
let s2 = { cpt = s2.cpt+1; cv_tbl = tbl } in
(* print_string (" >>> Creating CV" ^ (string_of_int (s2.cpt-1)) ^ "\n"); *)
(* flush stdout; *)
(s1, s2), clk
let rec (apply_subst:subst -> Eff.clock -> Eff.clock) =
fun (s1,s2) c ->
| On((cc,cv),clk) ->
let cv = match find_subst1 cv s1 with Some cv2 -> cv2 | None -> cv in
let clk = apply_subst (s1,s2) clk in
On((cc,cv), clk)
| ClockVar i ->
match find_subst2 i s2 with
| Some clk -> apply_subst (s1,s2) clk
| None -> c
(* apply only the second part of the subst *)
let rec (apply_subst2:subst -> Eff.clock -> Eff.clock) =
fun (s1,s2) c ->
match c with
| On(v,clk) ->
let clk = apply_subst2 (s1,s2) clk in
On(v, clk)
| ClockVar i ->
match find_subst2 i s2 with
| Some clk -> apply_subst2 (s1,s2) clk
| None -> c
let rec (apply_subst_val_exp : subst -> Eff.val_exp -> Eff.val_exp) =
fun s ve ->
let ve_core =
match ve.core with
| CallByPosEff (by_pos_op, OperEff vel) ->
let vel = List.map (apply_subst_val_exp s) vel in
CallByPosEff (by_pos_op, OperEff vel)
| CallByNameEff(by_name_op, fl) ->
let fl = List.map
(fun (fn,ve) -> (fn, apply_subst_val_exp s ve)) fl
in
CallByNameEff(by_name_op, fl)
in
let new_clk = List.map (apply_subst s) ve.clk in
let ve = { ve with core = ve_core ; clk = new_clk } in
ve
let is_clock_var = function
| On(_) | BaseEff -> false | ClockVar _ -> true
let (f : Lxm.t -> subst -> Eff.clock -> Eff.clock -> subst) =
fun lxm (s1,s2) ci1 ci2 ->
let ci1 = apply_subst (s1,s2) ci1 in
let ci2 = apply_subst (s1,s2) ci2 in
let rec aux (s1,s2) (c1,c2) =
match (c1,c2) with
| On(v,clk), BaseEff
| BaseEff, On(v,clk) -> (s1,s2)
(* not unifiable: we stop trying to find a substitution and return s;
the error message is issued outside [aux] (just below).
| BaseEff, BaseEff -> (s1,s2) (* ok *)
| On((cc1,cv1), clk1), On((cc2,cv2), clk2) ->
let s1 = if cv1 = cv2 then s1 else add_subst1 cv2 cv1 s1 in
aux (s1,s2) (clk1, clk2)
| ClockVar i, ClockVar j ->
if i=j then s1,s2 else s1,(add_link2 i j s2)
| ClockVar i, ci
| ci, ClockVar i -> s1, add_subst2 i ci s2
in
let s = aux (s1,s2) (ci1,ci2) in
let unifiable =
(* Two clocks are unifiable iff, once s have been applied, they are
equal, or one of them is a clock variable *)
let ci1 = apply_subst s ci1
and ci2 = apply_subst s ci2
in
ci1 = ci2 || is_clock_var ci1 || is_clock_var ci2
in
if unifiable then (
Verbose.print_string ~level:3 (
"# clock checking: unifying '" ^ (ci2str ci1) ^
"' and '" ^ (ci2str ci2) ^ "' -> "^ (subst_to_string s) ^"\n");
flush stdout;
s
)
else
let msg =
("\n*** clock error: The two following clocks are not unifiable:\n***\t" ^
(ci2str ci1) ^ "\n***\t" ^
(ci2str ci2) ^ "\n")
in
raise(Compile_error(lxm, msg))
(* exported *)
let (list : Lxm.t -> Eff.clock list -> subst -> Eff.clock * subst) =
fun lxm cl s ->
List.fold_left
(fun (clk,s) clk2 ->
let s = f lxm s clk clk2 in
let clk = apply_subst s clk in (* necessary? *)
(clk,s)
)
(List.hd cl, s)
(List.tl cl)
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
(******************************************************************************)
(* exported *)
let rec (const_to_val_eff: Lxm.t -> bool -> subst -> const -> subst * val_exp) =
fun lxm expand_const s const ->
let mk_by_pos_op by_pos_op_eff =
let s, clk = new_clock_var s in
{ core = CallByPosEff(flagit by_pos_op_eff lxm, OperEff []) ;
typ = [type_of_const const] ;
clk = [clk];
}
in
let id_of_int i = Ident.of_string (string_of_int i) in
match const with
| Bool_const_eff b ->
s, mk_by_pos_op (Predef((if b then Predef.TRUE_n else Predef.FALSE_n), []))
| Int_const_eff i ->
s, mk_by_pos_op (Predef((Predef.ICONST_n (id_of_int i)),[]))
| Real_const_eff r ->
s, mk_by_pos_op (Predef((Predef.RCONST_n (Ident.of_string r)),[]))
| Enum_const_eff (l, _)
| Extern_const_eff (l, _) -> s, mk_by_pos_op (IDENT (Ident.idref_of_long l))
| Abstract_const_eff (l, teff, c, is_exported) ->
if expand_const
then const_to_val_eff lxm expand_const s c
else s, mk_by_pos_op (IDENT (Ident.idref_of_long l))
| Array_const_eff (ct, _) ->
let s, vel =
List.fold_left
(fun (s,vel) c ->
let s,ve = const_to_val_eff lxm expand_const s c in
(s,ve::vel)
)
(s,[])
ct
in
let vel = List.rev vel in
s, mk_by_pos_op (ARRAY vel)
| Struct_const_eff (fl, stype) ->
let sname = match stype with
| Struct_type_eff(sname, _) -> sname
| _ -> assert false
in
let pack = Ident.pack_of_long sname in
let name_op_flg = flagit (STRUCT(pack, Ident.idref_of_long sname)) lxm in
let s, fl =
List.fold_left
(fun (s,fl) (id,const) ->
let s, ve = const_to_val_eff lxm expand_const s const in
s, (flagit id lxm, ve)::fl
)
(s,[])
fl
in
let fl = List.rev fl in
s, { core = (CallByNameEff(name_op_flg, fl));
typ = [stype] ;
clk = [BaseEff]
}