unifyClock.ml

(** 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)