Clock refactoring.

compiler/global/clocks.ml

@@ -0,0 +1,103 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Heptagon                                                              *)
+(*                                                                        *)
+(*  Author : Marc Pouzet                                                  *)
+(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
+(*                                                                        *)
+(**************************************************************************)
+
+open Names
+open Idents
+open Types
+
+type ct =
+  | Ck of ck
+  | Cprod of ct list
+
+and ck =
+  | Cbase
+  | Cvar of link ref
+  | Con of ck * constructor_name * var_ident
+
+and link =
+  | Cindex of int
+  | Clink of ck
+
+
+exception Unify
+
+
+let index = ref 0
+
+let gen_index () = (incr index; !index)
+
+(** returns a new clock variable *)
+let new_var () = Cvar { contents = Cindex (gen_index ()); }
+
+(** returns the canonic (short) representant of a [ck]
+    and update it to this value. *)
+let rec ck_repr ck = match ck with
+  | Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
+  | Cvar (({ contents = Clink ck } as link)) ->
+      let ck = ck_repr ck in (link.contents <- Clink ck; ck)
+
+
+(** verifies that index is fresh in ck. *)
+let rec occur_check index ck =
+  let ck = ck_repr ck in
+  match ck with
+    | Cbase -> ()
+    | Cvar { contents = Cindex n } when index <> n -> ()
+    | Con (ck, _, _) -> occur_check index ck
+    | _ -> raise Unify
+
+
+let rec unify t1 t2 =
+  if t1 == t2
+  then ()
+  else
+    (match (t1, t2) with
+       | (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
+       | (Cprod ct_list1, Cprod ct_list2) ->
+           (try List.iter2 unify ct_list1 ct_list2 with | _ -> raise Unify)
+       | _ -> raise Unify)
+
+and unify_ck ck1 ck2 =
+  let ck1 = ck_repr ck1 in
+  let ck2 = ck_repr ck2 in
+  if ck1 == ck2
+  then ()
+  else
+    (match (ck1, ck2) with
+       | (Cbase, Cbase) -> ()
+       | (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) when
+           n1 = n2 -> ()
+       | (Cvar (({ contents = Cindex n1 } as v)), _) ->
+           (occur_check n1 ck2; v.contents <- Clink ck2)
+       | (_, Cvar (({ contents = Cindex n2 } as v))) ->
+           (occur_check n2 ck1; v.contents <- Clink ck1)
+       | (Con (ck1, c1, n1), Con (ck2, c2, n2)) when (c1 = c2) & (n1 = n2) ->
+           unify_ck ck1 ck2
+       | _ -> raise Unify)
+
+
+let rec unify t1 t2 =
+  match (t1, t2) with
+    | (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
+    | (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list
+    | _ -> raise Unify
+
+and unify_list t1_list t2_list =
+  try List.iter2 unify t1_list t2_list with | _ -> raise Unify
+
+let rec skeleton ck = function
+  | Tprod ty_list -> Cprod (List.map (skeleton ck) ty_list)
+  | Tarray _ | Tid _ -> Ck ck
+
+let ckofct = function | Ck ck -> ck_repr ck | Cprod ct_list -> Cbase
+
+
+
+
+

compiler/heptagon/analysis/typing.ml

@@ -8,8 +8,6 @@
 (**************************************************************************)
 (* type checking *)
 
-(* $Id$ *)
-
 open Misc
 open Names
 open Idents

compiler/main/hept2mls.ml

@@ -15,6 +15,7 @@ open Names
 open Idents
 open Static
 open Types
+open Clocks
 open Format
 open Printf
 

compiler/minils/analysis/clocking.ml

@@ -14,6 +14,7 @@ open Minils
 open Mls_printer
 open Signature
 open Types
+open Clocks
 open Location
 open Printf
 
@@ -29,90 +30,8 @@ let err_message exp = function
         print_clock expected_ct;
       raise Error
 
-exception Unify
 
 
-
-let index = ref 0
-
-let gen_index () = (incr index; !index)
-
-let new_var () = Cvar { contents = Cindex (gen_index ()); }
-
-
-(** return the canonic representant form of a [ck] *)
-let rec repr ck = match ck with
-  | Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
-  | Cvar (({ contents = Clink ck } as link)) ->
-        let ck = repr ck in (link.contents <- Clink ck; ck)
-
-let rec occur_check index ck =
-  let ck = repr ck
-  in
-  match ck with
-    | Cbase -> ()
-    | Cvar { contents = Cindex n } when index <> n -> ()
-    | Con (ck, _, _) -> occur_check index ck
-    | _ -> raise Unify
-
-let rec ck_value ck =
-  match ck with
-    | Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
-    | Cvar { contents = Clink ck } -> ck_value ck
-
-let rec unify t1 t2 =
-  if t1 == t2
-  then ()
-  else
-    (match (t1, t2) with
-       | (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
-       | (Cprod ct_list1, Cprod ct_list2) ->
-           (try List.iter2 unify ct_list1 ct_list2 with | _ -> raise Unify)
-       | _ -> raise Unify)
-
-and unify_ck ck1 ck2 =
-  let ck1 = repr ck1 in
-  let ck2 = repr ck2 in
-  if ck1 == ck2
-  then ()
-  else
-    (match (ck1, ck2) with
-       | (Cbase, Cbase) -> ()
-       | (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) when
-           n1 = n2 -> ()
-       | (Cvar (({ contents = Cindex n1 } as v)), _) ->
-           (occur_check n1 ck2; v.contents <- Clink ck2)
-       | (_, Cvar (({ contents = Cindex n2 } as v))) ->
-           (occur_check n2 ck1; v.contents <- Clink ck1)
-       | (Con (ck1, c1, n1), Con (ck2, c2, n2)) when (c1 = c2) & (n1 = n2) ->
-           unify_ck ck1 ck2
-       | _ -> raise Unify)
-
-let rec eq ck1 ck2 =
-  match ((repr ck1), (repr ck2)) with
-    | (Cbase, Cbase) -> true
-    | (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) -> true
-    | (Con (ck1, _, n1), Con (ck2, _, n2)) when n1 = n2 -> eq ck1 ck2
-    | _ -> false
-
-let rec unify t1 t2 =
-  match (t1, t2) with
-    | (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
-    | (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list
-    | _ -> raise Unify
-
-and unify_list t1_list t2_list =
-  try List.iter2 unify t1_list t2_list with | _ -> raise Unify
-
-let rec skeleton ck = function
-  | Tprod ty_list -> Cprod (List.map (skeleton ck) ty_list)
-  | Tarray _ | Tid _ -> Ck ck
-
-let ckofct = function | Ck ck -> repr ck | Cprod ct_list -> Cbase
-
-let prod =
-  function | [] -> assert false | [ ty ] -> ty | ty_list -> Tprod ty_list
-
 let typ_of_name h x = Env.find x h
 
 let rec typing h e =
@@ -122,22 +41,20 @@ let rec typing h e =
     | Efby (c, e) -> typing h e
     | Eapp({a_op = op}, args, r) ->
         let ck = match r with
-        | None -> new_var ()
+          | None -> new_var ()
-        | Some(reset) -> typ_of_name h reset
+          | Some(reset) -> typ_of_name h reset in
-        in typing_op op args h e ck
+        typing_op op args h e ck
-     (* Typed exactly as a fun or a node... *)
+    | Eiterator (_, _, _, args, r) -> (* Typed exactly as a fun or a node... *)
-   | Eiterator (_, _, _, args, r) ->
+        let ck = match r with
-      let ck = match r with
+          | None -> new_var()
-        | None -> new_var()
+          | Some(reset) -> typ_of_name h reset
-        | Some(reset) -> typ_of_name h reset
+        in (List.iter (expect h (Ck ck)) args; skeleton ck e.e_ty)
-      in (List.iter (expect h (Ck ck)) args; skeleton ck e.e_ty)
     | Ewhen (e, c, n) ->
-        let ck_n = typ_of_name h n
+        let ck_n = typ_of_name h n in
-        in (expect h (skeleton ck_n e.e_ty) e;
+        (expect h (skeleton ck_n e.e_ty) e; skeleton (Con (ck_n, c, n)) e.e_ty)
-            skeleton (Con (ck_n, c, n)) e.e_ty)
     | Emerge (n, c_e_list) ->
-        let ck_c = typ_of_name h n
+        let ck_c = typ_of_name h n in
-        in (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty)
+        (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty)
     | Estruct l ->
         let ck = new_var () in
         (List.iter
@@ -148,7 +65,8 @@ let rec typing h e =
 and typing_op op args h e ck = match op, args with
   | (Efun _ | Enode _), e_list ->
       (List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty)
-  | Etuple, e_list -> Cprod (List.map (typing h) e_list)
+  | Etuple, e_list ->
+      Cprod (List.map (typing h) e_list)
   | Eifthenelse, [e1; e2; e3] ->
       let ct = skeleton ck e.e_ty
       in (expect h (Ck ck) e1; expect h ct e2; expect h ct e3; ct)
@@ -173,10 +91,8 @@ and typing_op op args h e ck = match op, args with
       in (expect h (Ck ck) e1; expect h ct e2; ct)
 
 
-
 and expect h expected_ty e =
-  let actual_ty = typing h e
+  let actual_ty = typing h e in
-  in
   try unify actual_ty expected_ty
   with | Unify -> err_message e (Etypeclash (actual_ty, expected_ty))
 
@@ -239,7 +155,7 @@ let typing_node ({ n_name = f;
   let h = build h l_list in
   (typing_eqs h eq_list;
    (*update clock info in variables descriptions *)
-   let set_clock vd = { vd with v_clock = ck_value (Env.find vd.v_ident h) } in
+   let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
    { (node) with
        n_input = List.map set_clock i_list;
        n_output = List.map set_clock o_list;

compiler/minils/minils.ml

@@ -15,6 +15,7 @@ open Idents
 open Signature
 open Static
 open Types
+open Clocks
 
 (** Warning: Whenever Minils ast is modified,
     minils_format_version should be incremented. *)
@@ -78,19 +79,6 @@ and op =
   | Elambda of var_dec list * var_dec list * var_dec list * eq list
       (* inputs, outputs, locals, body *)
 
-and ct =
-  | Ck of ck
-  | Cprod of ct list
-
-and ck =
-  | Cbase
-  | Cvar of link ref
-  | Con of ck * constructor_name * var_ident
-
-and link =
-  | Cindex of int
-  | Clink of ck
-
 and pat =
   | Etuplepat of pat list
   | Evarpat of var_ident

compiler/minils/mls_printer.ml

@@ -2,6 +2,7 @@
 open Names
 open Idents
 open Types
+open Clocks
 open Static
 open Format
 open Signature

compiler/minils/mls_utils.ml

@@ -7,6 +7,7 @@ open Idents
 open Signature
 open Static
 open Types
+open Clocks
 open Misc
 
 (** Error Kind *)

compiler/minils/transformations/normalize.ml

@@ -13,6 +13,7 @@ open Signature
 open Minils
 open Mls_utils
 open Types
+open Clocks
 
 let ctrue = Name "true"
 and cfalse = Name "false"

compiler/obc/control.ml

@@ -14,6 +14,7 @@ open Minils
 open Idents
 open Misc
 open Obc
+open Clocks
 
 let var_from_name map x =
   begin try