Source file unifyClock.ml

(* Time-stamp: <modified the 29/08/2019 (at 16:47) by Erwan Jahier> *)

(* XXX a revoir et faire comme expliqué ici :
http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec26-type-inference/type-inference.htm

   C'est peu ou prou, ce que je fais, mais bon, j'ai plus trop confiance
   dans ce module, et il mériterait un bon nettoyage.

   Un truc louche, c'est que je pretend utiliser de l'unification
   pour vérifier les appels de noeud, en cherchant à unifier les
   parametres et les arguments. Mais, me semble-t'il, cette
   vérification est orientée (ca ne marche que si on fait "f par arg"
   (ou le contraire). Et cette dissymétrie n'apparait ni dans le mli,
   ni dans le terme unify.

   Par ailleur, subst devrait s'appeler env (en reminiscence des
   environnements de types).

*)
open Lxm
open Lv6errors
open Lic

(** DEBUG FLAG *)
let dbg = (Lv6Verbose.get_flag "clock-check2")


let ci2str = LicDump.string_of_clock2

(* exported *)
type subst1 = (Lv6Id.t * Lv6Id.t) list

(**
   A dedicated kind of substitution tailored to deal with clock variables 
   (Lic.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 Lic.clock type
   that materialize this fact).
   
   - When unifying two Lic.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 " ; " 
       (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 -> ("CV"^(string_of_int i))::acc) is [])) ^
                "}"
            )::acc
          )
          s2.cv_tbl
          []
       )) 

let (subst_to_string : subst -> string) = 
  fun (s1,s2) -> 
    let v2s = Lv6Id.to_string in
    let s2str = subst2_to_string s2 in
    let s1str = 
      (String.concat ", " (List.map (fun (v1,v2) -> (v2s v1) ^ "->" ^ (v2s v2)) s1))
    in
    if s2str = "" then s2str else if s1str = "" then s2str else
       (s1str ^" ; " ^ s2str)
        
(******************************************************************************)

(* exported *)
let (empty_subst2:subst2) = { cpt = 0 ; cv_tbl = IntMap.empty }
let (empty_subst:subst) = [], empty_subst2

let (_add_subst1 : Lv6Id.t -> Lv6Id.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 -> Lic.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 : Lv6Id.t -> subst1 -> Lv6Id.t option) =
  fun id s ->
    try Some (List.assoc id s) with Not_found -> None

let (find_subst2 : int -> subst2 -> Lic.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 * Lic.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


(* exported *)
let rec (apply_subst:subst -> Lic.clock -> Lic.clock) =
  fun (s1,s2) c ->
    match c with
      | BaseLic -> BaseLic
      | On((cc,cv,ct),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,ct),  clk)
      | ClockVar i ->
        match find_subst2 i s2 with
          | Some clk -> apply_subst (s1,s2) clk
          | None -> c


(* exported *)
(* apply only the second part of the subst *)
let rec (apply_subst2:subst -> Lic.clock -> Lic.clock) =
  fun (s1,s2) c ->
    match c with
      | BaseLic -> BaseLic 
      | 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 -> Lic.val_exp -> Lic.val_exp) =
  fun s ve ->
    let ve_core = 
      match ve.ve_core with
        | CallByPosLic (by_pos_op, vel) -> 
          let vel = List.map (apply_subst_val_exp s) vel in
          CallByPosLic (by_pos_op, vel)
        | CallByNameLic(by_name_op, fl) -> 
          let fl = List.map
            (fun (fn,ve) -> (fn, apply_subst_val_exp s ve)) fl
          in
          CallByNameLic(by_name_op, fl)
        | Merge(ce,cl) -> 
          let cl = List.map
            (fun (fn,ve) -> (fn, apply_subst_val_exp s ve)) cl
          in
          Merge(ce, cl) 
    in
    let new_clk = List.map (apply_subst s) ve.ve_clk in
    let ve = { ve with ve_core = ve_core ; ve_clk = new_clk } in
    ve


let is_clock_var = function 
  | On(_) | BaseLic -> false | ClockVar _ -> true
  
(* exported 

It's not really an unification algo, but rather a « compatibility checking ».
By compatibility, I mean that, 
- c1 = c2
- c1 or c2 are clock var
- if c1=On(id1,cc1) and c2=On(id2,cc2) then
   cc1 and cc1[id1/id2] are compatible
*)

let (f : subst -> Lxm.t -> Lic.clock -> Lic.clock -> subst) =
  fun (s1,s2) lxm  arg par -> 
    let arg = apply_subst (s1,s2) arg in
    let par = apply_subst (s1,s2) par in
    let rec aux (s1,s2) (c1,c2) = 
      match (c1,c2) with
	     | On(_v,_clk), BaseLic
	     | BaseLic, 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).
	     *)
	     | BaseLic, BaseLic -> (s1,s2) (* ok *)
	     | On((cc1,cv1,_), clk1), On((cc2,cv2,_), clk2) ->
           if (cc1,cv1) = (cc2,cv2) then aux (s1,s2) (clk1, clk2) else (s1,s2)
	     | 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) (arg,par) in
    let compatible =
      (* Two clocks are compatible if, once s have been applied, they are
         equal, or one of them is a clock variable *)
      let npar = apply_subst s par
      and narg = apply_subst s arg in
      narg = npar || is_clock_var narg || is_clock_var npar
    in
    if s <> (s1,s2) then
      Lv6Verbose.exe
        ~flag:dbg
        (fun () ->
 	      print_string (
	          "# UnifyClock.f ("^(Lxm.position lxm)^"), unifying \n#\t -" ^ (ci2str arg) ^
	            " \n#\t -" ^ (ci2str par) ^ "\n# produces s = " ^ (subst_to_string s)^
                 "\n# out of   s = " ^ (subst_to_string (s1,s2))^
                   "\n"
           );
         flush stdout;
        );
    if compatible then s else
	   let msg =  
	     ("\n*** clock error: The two following clocks are not compatible:\n***\t" ^ 
	         (ci2str arg) ^ " (provided clock)\n***\t" ^ 
	         (ci2str par) ^ " (expected clock)\n")
	   in
	   raise(Compile_error(lxm, msg))


(* exported *)
let (list : Lxm.t list -> Lic.clock list -> subst -> subst) =
  fun lxms cl s ->
  if cl = [] then s 
  else (
    assert(lxms<>[]);
    snd(
    List.fold_left2
      (fun (clk,s) lxm clk2 ->
	     let s = f s lxm clk clk2 in
	     let clk = apply_subst s clk in (* necessary? *)
	     (clk,s)
      )
      (List.hd cl, s)
      (List.tl lxms)
      (List.tl cl)
  ))


(******************************************************************************)
(* exported *)
(* This function is in this module to avoid to export new_clock_var. A good idea? *)
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_arg by_pos_op_eff arg =
      let _s,clk = match const with
	     | Tuple_const_eff cl ->
          let f (s,clks) _c =  
            let s, clk = new_clock_var s in
            (s,clk::clks)
          in
          List.fold_left f (s,[]) cl

	     | _c ->
          let s, clk = new_clock_var s in
          s, [clk]
      in
      { ve_core = CallByPosLic(flagit by_pos_op_eff lxm, arg) ; 
        ve_typ = types_of_const const ;
        ve_clk = clk;
        ve_src = lxm
      }
    in
    let mk_by_pos_op by_pos_op_eff = mk_by_pos_op_arg by_pos_op_eff [] in
    match const with
    | Bool_const_eff _ 
    | Int_const_eff  _
    | Real_const_eff _ -> s, mk_by_pos_op (CONST const)
    | Enum_const_eff   (l, _)
    | Extern_const_eff (l, _) -> s, mk_by_pos_op (CONST_REF 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 (CONST_REF 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_arg ARRAY vel
    | Tuple_const_eff cl ->
      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,[])
          cl
      in
      let vel = List.rev vel in
      s, mk_by_pos_op_arg TUPLE vel
    | Struct_const_eff (fl, stype) ->
      let sname = match stype with 
        | Struct_type_eff(sname, _) -> sname
        | _ -> assert false
      in
      let name_op_flg = flagit (STRUCT(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, { ve_core = (CallByNameLic(name_op_flg, fl));
           ve_typ = [stype] ;
           ve_clk = [BaseLic];
           ve_src = lxm
         }