-
Erwan Jahier authored
as many new local variables as necessary so that an expression is made at most of one operator. The rational for that is to obtain a lic code that is trivial to clock check (nested node calls, for example, make it less simple). The old behavior can still be obtained using --keep-nested-calls. During that change, I realised that I did not clock check asserts. Hence, I have also added this check.
Erwan Jahier authoredas many new local variables as necessary so that an expression is made at most of one operator. The rational for that is to obtain a lic code that is trivial to clock check (nested node calls, for example, make it less simple). The old behavior can still be obtained using --keep-nested-calls. During that change, I realised that I did not clock check asserts. Hence, I have also added this check.
unifyClock.ml 3.17 KiB
(** Time-stamp: <modified the 19/08/2008 (at 09:26) by Erwan Jahier> *)
open SyntaxTree
open SyntaxTreeCore
open CompiledData
open LicDump
open Printf
open Lxm
open Errors
let ci2str = LicDump.string_of_clock2
(* exported *)
type subst = (Ident.t * Ident.t) list * (int * clock_eff) list
(* exported *)
let (empty_subst:subst) = [],[]
(******************************************************************************)
(* Stuff to generate fresh clock vars *)
let var_type = ref 0
let reset_var_type () = var_type := 0
let (get_var_type : unit -> int) =
fun () -> incr var_type; !var_type
(* exported *)
let (get_constant_clock : unit -> clock_eff) =
fun () -> ClockVar (get_var_type ())
(******************************************************************************)
let subst_to_string (s1,s2) =
let v2s v = Ident.to_string v in
(String.concat ", " (List.map (fun (v1,v2) -> (v2s v1) ^ "/" ^ (v2s v2)) s1)) ^
" + " ^
(String.concat ", " (List.map (fun (v1,v2) -> (string_of_int v1) ^ "/" ^
(ci2str v2)) s2))
(* exported *)
let rec (apply_subst:subst -> clock_eff -> clock_eff) =
fun (s1,s2) c ->
match c with
| BaseEff -> BaseEff
| On(v,clk) ->
let v = try List.assoc v s1 with Not_found -> v in
On(v, apply_subst (s1,s2) clk)
| ClockVar i ->
try apply_subst (s1,s2) (List.assoc i s2)
with Not_found -> c
(* exported *)
let (f : Lxm.t -> subst -> clock_eff -> clock_eff -> 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) arg = match arg 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 will be issued outside [aux].
*)
| BaseEff, BaseEff -> (s1,s2) (* ok *)
| On(v1,clk1), On(v2,clk2) ->
let s1 = if v1 = v2 then s1 else ((v2,v1)::s1) in
aux (s1,s2) (clk1, clk2) | ClockVar i, ClockVar j -> if i<>j then s1,((i,ClockVar j)::s2) else s1,s2
| ClockVar i, ci
| ci, ClockVar i -> s1,((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 modulo the left-most hand-side *)
match apply_subst s ci1, apply_subst s ci2 with
| On(_,c1),On(_,c2) -> c1 = c2
| BaseEff, BaseEff -> true
| BaseEff,On(_,_)
| On(_,_),BaseEff -> false
| ClockVar _, _
| _, ClockVar _ -> true
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 expression has clock '" ^
(ci2str ci1) ^ "', \n*** but it is used with clock '" ^
(ci2str ci2) ^ "'.\n"
in
raise(Compile_error(lxm, msg))
(* exported *)
let (list : Lxm.t -> clock_eff list -> subst -> clock_eff * 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)