From dc9bec28bfdccd9ec5aa35398e27934c9868975c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Le=CC=81onard=20Ge=CC=81rard?= Date: Fri, 23 Jul 2010 22:06:06 +0200 Subject: [PATCH] Clock refactoring. --- compiler/global/clocks.ml | 103 ++++++++++++++++ compiler/heptagon/analysis/typing.ml | 2 - compiler/main/hept2mls.ml | 1 + compiler/minils/analysis/clocking.ml | 118 +++---------------- compiler/minils/minils.ml | 14 +-- compiler/minils/mls_printer.ml | 1 + compiler/minils/mls_utils.ml | 1 + compiler/minils/transformations/normalize.ml | 1 + compiler/obc/control.ml | 1 + 9 files changed, 126 insertions(+), 116 deletions(-) create mode 100644 compiler/global/clocks.ml diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml new file mode 100644 index 0000000..4519834 --- /dev/null +++ b/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 + + + + + diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 365541e..5ee9e6c 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -8,8 +8,6 @@ (**************************************************************************) (* type checking *) -(* $Id$ *) - open Misc open Names open Idents diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 2e80156..f9b5370 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -15,6 +15,7 @@ open Names open Idents open Static open Types +open Clocks open Format open Printf diff --git a/compiler/minils/analysis/clocking.ml b/compiler/minils/analysis/clocking.ml index 0f789ce..a5da1af 100644 --- a/compiler/minils/analysis/clocking.ml +++ b/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 () - | Some(reset) -> typ_of_name h reset - in typing_op op args h e ck - (* Typed exactly as a fun or a node... *) - | Eiterator (_, _, _, args, r) -> - let ck = match r with - | None -> new_var() - | Some(reset) -> typ_of_name h reset - in (List.iter (expect h (Ck ck)) args; skeleton ck e.e_ty) + | None -> new_var () + | Some(reset) -> typ_of_name h reset in + typing_op op args h e ck + | Eiterator (_, _, _, args, r) -> (* Typed exactly as a fun or a node... *) + let ck = match r with + | None -> new_var() + | Some(reset) -> typ_of_name h reset + 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 - in (expect h (skeleton ck_n e.e_ty) e; - skeleton (Con (ck_n, c, n)) e.e_ty) + let ck_n = typ_of_name h n in + (expect h (skeleton ck_n e.e_ty) e; skeleton (Con (ck_n, c, n)) e.e_ty) | Emerge (n, c_e_list) -> - let ck_c = typ_of_name h n - in (typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty) + let ck_c = typ_of_name h n in + (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 - in + let actual_ty = typing h e 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; diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index 8909006..cd19a33 100644 --- a/compiler/minils/minils.ml +++ b/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 diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 1fb7994..065d042 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -2,6 +2,7 @@ open Names open Idents open Types +open Clocks open Static open Format open Signature diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 724d6db..8d953dd 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -7,6 +7,7 @@ open Idents open Signature open Static open Types +open Clocks open Misc (** Error Kind *) diff --git a/compiler/minils/transformations/normalize.ml b/compiler/minils/transformations/normalize.ml index 515f67f..fcd31a3 100644 --- a/compiler/minils/transformations/normalize.ml +++ b/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" diff --git a/compiler/obc/control.ml b/compiler/obc/control.ml index 9527210..5645a02 100644 --- a/compiler/obc/control.ml +++ b/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