From 9f72564c94a5d48802c869c68985d1e904e006f1 Mon Sep 17 00:00:00 2001 From: Erwan Jahier <jahier@imag.fr> Date: Thu, 26 Jun 2008 17:37:07 +0200 Subject: [PATCH] Cosmetic change: change the CompiledData.clock_eff to what was called clock_info, and therefore also remove clock_info. The rationale of this change is that it makes things slightly simpler, and more homogeneous with what is done in type checking. --- src/compiledData.ml | 5 ++- src/compiledDataDump.ml | 20 +++++++--- src/evalClock.ml | 87 +++++++++++++++++++---------------------- src/evalClock.mli | 8 ++-- src/getEff.ml | 15 +++---- src/getEff.mli | 4 +- src/lazyCompiler.ml | 4 +- src/unifyClock.ml | 70 ++++++++++++--------------------- src/unifyClock.mli | 23 +++-------- 9 files changed, 105 insertions(+), 131 deletions(-) diff --git a/src/compiledData.ml b/src/compiledData.ml index 1bddaca7..29a56e99 100644 --- a/src/compiledData.ml +++ b/src/compiledData.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 17/06/2008 (at 10:10) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/06/2008 (at 16:56) by Erwan Jahier> *) (** @@ -245,7 +245,8 @@ and var_info_eff = { } and clock_eff = | BaseEff (* it's not bezef... *) - | On of var_info_eff (* nb: it is recursive *) + | On of Ident.t * clock_eff + | ClockVar of int (* to deal with polymorphic clocks (i.e., constants) *) (**********************************************************************************) (** [node_exp_eff] correspond à une instance de template (ou, cas diff --git a/src/compiledDataDump.ml b/src/compiledDataDump.ml index db77462c..2eec9650 100644 --- a/src/compiledDataDump.ml +++ b/src/compiledDataDump.ml @@ -325,15 +325,25 @@ and (node_of_node_exp_eff: node_exp_eff -> string) = and string_of_clock2 (ck : clock_eff) = - match ck with - | BaseEff -> " on base " - | On veff ->" on " ^ (Ident.to_string veff.var_name_eff) ^ - (string_of_clock veff.var_clock_eff) + let rec string_of_clock2_aux ck = + (* to avoid printing the first level var name *) + match ck with + | BaseEff -> " on base" + | On(veff,ceff) ->" on " ^ (Ident.to_string veff) ^ + (string_of_clock2_aux ceff) + | ClockVar i -> "'a" ^ string_of_int i + in + match ck with + | BaseEff -> " on base" + | On(_,ceff) -> (string_of_clock2_aux ceff) + | ClockVar i -> "'a" ^ string_of_int i and string_of_clock (ck : clock_eff) = match ck with | BaseEff -> "" - | On veff ->" when " ^ (Ident.to_string veff.var_name_eff) + | On(_,BaseEff) -> "" + | On(v,On(id,_)) ->" when " ^ (Ident.to_string id) + | _ -> assert false and string_of_clock_list cl = diff --git a/src/evalClock.ml b/src/evalClock.ml index e611f6fe..a46d4602 100644 --- a/src/evalClock.ml +++ b/src/evalClock.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 26/06/2008 (at 16:24) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/06/2008 (at 17:36) by Erwan Jahier> *) open Predef @@ -59,7 +59,7 @@ open UnifyClock *) -let (check_args : Lxm.t -> subst -> clock_info list -> clock_info list -> subst) = +let (check_args : Lxm.t -> subst -> clock_eff list -> clock_eff list -> subst) = fun lxm s cil_par cil_arg -> assert (List.length cil_par = List.length cil_arg); let s = List.fold_left2 (UnifyClock.f lxm) s cil_par cil_arg in @@ -69,7 +69,7 @@ let (check_args : Lxm.t -> subst -> clock_info list -> clock_info list -> subst) -------------------------- It is the same thing, except that we have left_eff list instead - of clock_info list. + of clock_eff list. e.g., in the equation: @@ -108,11 +108,13 @@ let rec (var_info_eff_of_left_eff: left_eff -> var_info_eff) = { v with var_name_eff = Ident.of_string new_name } +let var_info_eff_to_clock_eff v = v.var_clock_eff + (* exported *) -let (check_res : Lxm.t -> subst -> left_eff list -> clock_info list -> unit) = +let (check_res : Lxm.t -> subst -> left_eff list -> clock_eff list -> unit) = fun lxm s left rigth -> let left_vi = List.map var_info_eff_of_left_eff left in - let left_ci = List.map var_info_eff_to_clock_info left_vi in + let left_ci = List.map var_info_eff_to_clock_eff left_vi in if (List.length left_ci <> List.length rigth) then raise (Compile_error(lxm, "!!!")); ignore(List.fold_left2 (UnifyClock.f lxm) s left_ci rigth) @@ -125,24 +127,24 @@ let (check_res : Lxm.t -> subst -> left_eff list -> clock_info list -> unit) = (** In order to clock check "when" statements, we need to know if a clock [sc] is a sub_clock of another one c (i.e., for all instants i, c(i) => sc(i)) *) -let rec (is_a_sub_clock : Lxm.t -> subst -> clock_info -> clock_info -> subst option) = +let rec (is_a_sub_clock : Lxm.t -> subst -> clock_eff -> clock_eff -> subst option) = fun lxm s sc c -> (* check if [sc] is a sub-clock of [c] (in the large sens). Returns Some updated substitution if it is the case, and None otherwise *) match sc,c with (* the base clock is a sub-clock of all clocks *) - | Ci_base, (Ci_base|Ci_on(_,_)|Ci_var _) -> Some s + | BaseEff, (BaseEff|On(_,_)|ClockVar _) -> Some s - | Ci_on(v,clk), Ci_base -> None - | Ci_on(v,clk), Ci_on(v2,clk2) -> ( + | On(v,clk), BaseEff -> None + | On(v,clk), On(v2,clk2) -> ( try Some(UnifyClock.f lxm s clk clk2) with _ -> is_a_sub_clock lxm s sc clk2 ) - | Ci_var j, Ci_base -> assert false + | ClockVar j, BaseEff -> assert false - | Ci_var i, Ci_on(_,_) - | Ci_var i, Ci_var _ -> + | ClockVar i, On(_,_) + | ClockVar i, ClockVar _ -> (* XXX can it occur? if yes, something should be done the problem being that several things are possible (there is no unique sub-clock of a clock... @@ -153,19 +155,19 @@ let rec (is_a_sub_clock : Lxm.t -> subst -> clock_info -> clock_info -> subst op let s1,s2 = s in Some (s1,(i,c)::s2) - | Ci_on(_,_), Ci_var i -> (* Ditto *) + | On(_,_), ClockVar i -> (* Ditto *) let s1,s2 = s in Some (s1,(i,sc)::s2) -type clock_profile = clock_info list * clock_info list +type clock_profile = clock_eff list * clock_eff list let (get_clock_profile : node_exp_eff -> clock_profile) = fun n -> - (List.map var_info_eff_to_clock_info n.inlist_eff, - List.map var_info_eff_to_clock_info n.outlist_eff) + (List.map var_info_eff_to_clock_eff n.inlist_eff, + List.map var_info_eff_to_clock_eff n.outlist_eff) -let ci2str = string_of_clock_info +let ci2str = CompiledDataDump.string_of_clock2 (******************************************************************************) (* Stuff to generated fresh var clocks *) @@ -176,25 +178,18 @@ let get_var_type () = incr var_type; !var_type let cpt_var_name = ref 0 -let (make_dummy_var: string -> var_info_eff) = +let (make_dummy_var: string -> Ident.t) = fun str -> - let id = Ident.of_string (str ^ (string_of_int !cpt_var_name)) in - { - var_name_eff = id; - var_nature_eff = VarLocal; - var_number_eff = -1; - var_type_eff = Bool_type_eff; - var_clock_eff = BaseEff; - } - -let get_constant_clock () = Ci_var (get_var_type ()) -(* Ci_on(make_dummy_var "const",Ci_var (get_var_type ())) *) + Ident.of_string (str ^ (string_of_int !cpt_var_name)) + +let get_constant_clock () = ClockVar (get_var_type ()) +(* On(make_dummy_var "const",ClockVar (get_var_type ())) *) let concat_subst (s11,s12) (s21,s22) = (s11 @ s21, s12@s22) (******************************************************************************) -let rec (f : id_solver -> subst -> val_exp_eff -> clock_info list * subst) = +let rec (f : id_solver -> subst -> val_exp_eff -> clock_eff list * subst) = fun id_solver s ve -> cpt_var_name := 0; reset_var_type (); @@ -213,7 +208,7 @@ and f_aux id_solver s ve = (* iterate f on a list of expression *) -and (f_list : id_solver -> subst -> val_exp_eff list -> clock_info list list * subst) = +and (f_list : id_solver -> subst -> val_exp_eff list -> clock_eff list list * subst) = fun id_solver s args -> let aux (acc,s) arg = let cil, s = f_aux id_solver s arg in @@ -223,14 +218,14 @@ and (f_list : id_solver -> subst -> val_exp_eff list -> clock_info list list * s List.rev cil, s and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list -> - subst -> clock_info list * subst) = + subst -> clock_eff list * subst) = fun id_solver posop lxm args s -> match posop with | CURRENT_eff -> ( (* we return the clock of the argument *) let clocks_of_args, s = f_list id_solver s args in match List.flatten clocks_of_args with - | [Ci_base] -> [Ci_base],s - | [Ci_on(_,clk)] -> [clk],s + | [BaseEff] -> [BaseEff],s + | [On(_,clk)] -> [clk],s | _ -> assert false ) | WHEN_eff -> ( @@ -252,13 +247,13 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list try (id_solver.id2var id2 lxm2) with _ -> assert false in - let clk = var_info_eff_to_clock_info clk_var in + let clk = var_info_eff_to_clock_eff clk_var in let clk_of_c1,s = match c1 with - | Ci_base -> assert false - | Ci_on(var,_) -> Ci_on(var, clk), s - | Ci_var i -> - let cc1 = Ci_on(make_dummy_var "const",clk) in + | BaseEff -> assert false + | On(var,_) -> On(var, clk), s + | ClockVar i -> + let cc1 = On(make_dummy_var "const",clk) in let (s1,s2) = s in cc1, (s1,(i,cc1)::s2) in @@ -279,7 +274,7 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list | Predef_eff (TRUE_n,_) | Predef_eff (FALSE_n,_) -> [get_constant_clock ()],s | IDENT_eff idref -> ( - try ([var_info_eff_to_clock_info (id_solver.id2var idref lxm)], s) + try ([var_info_eff_to_clock_eff (id_solver.id2var idref lxm)], s) with _ -> (* => it is a constant *) [get_constant_clock ()],s ) | CALL_eff node_exp_eff -> @@ -290,15 +285,15 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list Hence we create a fresh var clock, that will be instanciated by the caller. *) - let rel_base = Ci_var (get_var_type ()) in - let rec (replace_base : clock_info -> clock_info -> clock_info) = + let rel_base = ClockVar (get_var_type ()) in + let rec (replace_base : clock_eff -> clock_eff -> clock_eff) = fun rel_base ci -> (* [replace_base rel_base ci ] replaces in [ci] any occurences of the base clock by [rel_base] *) match ci with - | Ci_base -> rel_base - | Ci_on(v,clk) -> Ci_on(v, replace_base rel_base clk) - | Ci_var i -> ci + | BaseEff -> rel_base + | On(v,clk) -> On(v, replace_base rel_base clk) + | ClockVar i -> ci in let cil_arg = List.map (replace_base rel_base) cil_arg in let cil_res = List.map (replace_base rel_base) cil_res in @@ -351,7 +346,7 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list and (eval_by_name_clock : id_solver -> by_name_op_eff -> Lxm.t -> (Ident.t Lxm.srcflagged * val_exp_eff) list -> subst -> - clock_info list * subst) = + clock_eff list * subst) = fun id_solver namop lxm namargs s -> match namop with | STRUCT_anonymous_eff -> assert false (* cf EvalType.f *) diff --git a/src/evalClock.mli b/src/evalClock.mli index 14bc8c64..abedd24e 100644 --- a/src/evalClock.mli +++ b/src/evalClock.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 26/06/2008 (at 14:59) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/06/2008 (at 16:35) by Erwan Jahier> *) open CompiledData open UnifyClock @@ -8,7 +8,7 @@ open UnifyClock and returns a clock profile that contains all the necessary information to be able to check. *) -val f : id_solver -> subst -> val_exp_eff -> clock_info list * subst +val f : id_solver -> subst -> val_exp_eff -> clock_eff list * subst (** [check_res lxm cel cil] check that the expected output clock @@ -22,11 +22,11 @@ val f : id_solver -> subst -> val_exp_eff -> clock_info list * subst it checks that the clock of "(x,y)" (cel) is compatible with the output clock profile of node toto (cil). - The type [clock_info_res] is exported to be able to call that + The type [clock_eff_res] is exported to be able to call that function outside this module, which is necessary to clock equations (an equation is not an expression (i.e., not a val_exp_eff). *) -val check_res : Lxm.t -> subst -> left_eff list -> clock_info list -> unit +val check_res : Lxm.t -> subst -> left_eff list -> clock_eff list -> unit diff --git a/src/getEff.ml b/src/getEff.ml index 82d3550b..a435354b 100644 --- a/src/getEff.ml +++ b/src/getEff.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 26/06/2008 (at 15:01) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/06/2008 (at 17:31) by Erwan Jahier> *) open Lxm @@ -33,12 +33,13 @@ let rec (typ:CompiledData.id_solver -> SyntaxTreeCore.type_exp -> raise (Compile_error(texp.src, "can't eval type: "^msg)) (* exported *) -let rec (clock : CompiledData.id_solver -> SyntaxTreeCore.clock_exp -> - CompiledData.clock_eff)= - fun id_solver cexp -> - match cexp with - | Base -> BaseEff - | NamedClock id -> On (id_solver.id2var (Ident.to_idref id.it) id.src) +let rec (clock : CompiledData.id_solver -> var_info -> CompiledData.clock_eff)= + fun id_solver v -> + match v.var_clock with + | Base -> On(v.var_name,BaseEff) + | NamedClock id -> + let id_v = id_solver.id2var (Ident.to_idref id.it) id.src in + On(v.var_name, id_v.var_clock_eff) (******************************************************************************) diff --git a/src/getEff.mli b/src/getEff.mli index cc6a5826..cae840f5 100644 --- a/src/getEff.mli +++ b/src/getEff.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 09/06/2008 (at 11:27) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/06/2008 (at 16:52) by Erwan Jahier> *) (** This module defines functions that translate SyntaxTreeCore datatypes into @@ -14,7 +14,7 @@ *) val typ : CompiledData.id_solver -> SyntaxTreeCore.type_exp -> CompiledData.type_eff -val clock: CompiledData.id_solver -> SyntaxTreeCore.clock_exp -> CompiledData.clock_eff +val clock: CompiledData.id_solver -> SyntaxTreeCore.var_info -> CompiledData.clock_eff (** A [node_exp] is a name plus a list of static arguments. diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml index c4b27260..a136bde2 100644 --- a/src/lazyCompiler.ml +++ b/src/lazyCompiler.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 26/06/2008 (at 14:49) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/06/2008 (at 16:48) by Erwan Jahier> *) open Lxm @@ -561,7 +561,7 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t -> let type_args id = let vi = Hashtbl.find vars.vartable id in let t_eff = GetEff.typ node_id_solver vi.it.var_type in - let c_eff = GetEff.clock node_id_solver vi.it.var_clock in + let c_eff = GetEff.clock node_id_solver vi.it in let vi_eff = { var_name_eff = vi.it.var_name; var_nature_eff = vi.it.var_nature; diff --git a/src/unifyClock.ml b/src/unifyClock.ml index f0230196..93496085 100644 --- a/src/unifyClock.ml +++ b/src/unifyClock.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 26/06/2008 (at 15:17) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/06/2008 (at 16:58) by Erwan Jahier> *) open SyntaxTree @@ -9,87 +9,65 @@ open Printf open Lxm open Errors -(* exported *) -type clock_info = - | Ci_base - | Ci_on of var_info_eff * clock_info - | Ci_var of int (* to deal with polymorphic clocks (i.e., constants) *) - -(* exported *) -let rec (var_info_eff_to_clock_info:var_info_eff -> clock_info) = - fun v -> - match v.var_clock_eff with - | BaseEff -> Ci_on(v, Ci_base) - | On clk -> Ci_on(v, var_info_eff_to_clock_info clk) - -let rec (string_of_clock_info:clock_info -> string) = function - | Ci_var i -> "'a" ^ string_of_int i - | Ci_base -> "base" - | Ci_on (v,clk) -> " on " ^ (aux clk) -and aux = function - | Ci_var i -> "'a" ^ string_of_int i - | Ci_base -> "base" - | Ci_on (v,clk) -> (Ident.to_string v.var_name_eff) ^ " on " ^ (aux clk) -let ci2str = string_of_clock_info +let ci2str = CompiledDataDump.string_of_clock2 (* exported *) -type subst = - (var_info_eff * var_info_eff) list * (int * clock_info) list +type subst = (Ident.t * Ident.t) list * (int * clock_eff) list (* exported *) let (empty_subst:subst) = [],[] let subst_to_string (s1,s2) = - let v2s v = Ident.to_string v.var_name_eff in + 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_info -> clock_info) = +let rec (apply_subst:subst -> clock_eff -> clock_eff) = fun (s1,s2) c -> match c with - | Ci_base -> Ci_base - | Ci_on(v,clk) -> + | BaseEff -> BaseEff + | On(v,clk) -> let v = try List.assoc v s1 with Not_found -> v in - Ci_on(v, apply_subst (s1,s2) clk) - | Ci_var i -> + 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_info -> clock_info -> subst) = +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 - | Ci_on(v,clk), Ci_base - | Ci_base, Ci_on(v,clk) -> (s1,s2) + | 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]. *) - | Ci_base, Ci_base -> (s1,s2) (* ok *) - | Ci_on(v1,clk1), Ci_on(v2,clk2) -> + | 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) - | Ci_var i, Ci_var j -> if i<>j then s1,((i,Ci_var j)::s2) else s1,s2 - | Ci_var i, ci - | ci, Ci_var i -> s1,((i,ci)::s2) + | 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 - | Ci_on(_,c1),Ci_on(_,c2) -> c1 = c2 - | Ci_base, Ci_base -> true - | Ci_base,Ci_on(_,_) - | Ci_on(_,_),Ci_base -> false - | Ci_var _, _ - | _, Ci_var _ -> true + | 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 ( @@ -107,7 +85,7 @@ let (f : Lxm.t -> subst -> clock_info -> clock_info -> subst) = raise(Compile_error(lxm, msg)) (* exported *) -let (list : Lxm.t -> clock_info list -> subst -> clock_info * subst) = +let (list : Lxm.t -> clock_eff list -> subst -> clock_eff * subst) = fun lxm cl s -> List.fold_left (fun (clk,s) clk2 -> diff --git a/src/unifyClock.mli b/src/unifyClock.mli index 8abed5e9..14a28162 100644 --- a/src/unifyClock.mli +++ b/src/unifyClock.mli @@ -1,17 +1,7 @@ -(** Time-stamp: <modified the 26/06/2008 (at 15:16) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/06/2008 (at 16:58) by Erwan Jahier> *) open CompiledData -type clock_info = - | Ci_base - | Ci_on of var_info_eff * clock_info - | Ci_var of int (* to deal with polymorphic clocks (i.e., constants) *) - - -(** a few conversion function *) - -val var_info_eff_to_clock_info:var_info_eff -> clock_info -val string_of_clock_info:clock_info -> string (* XXX use Map.t @@ -35,14 +25,13 @@ val string_of_clock_info:clock_info -> string XXX Make it abstract *) -type subst = - (var_info_eff * var_info_eff) list * (int * clock_info) list +type subst = (Ident.t * Ident.t) list * (int * clock_eff) list val empty_subst : subst -val apply_subst:subst -> clock_info -> clock_info +val apply_subst:subst -> clock_eff -> clock_eff -(** Raises an error is the 2 clock_info are not unifiable *) -val f : Lxm.t -> subst -> clock_info -> clock_info -> subst -val list : Lxm.t -> clock_info list -> subst -> clock_info * subst +(** Raises an error is the 2 clock_eff are not unifiable *) +val f : Lxm.t -> subst -> clock_eff -> clock_eff -> subst +val list : Lxm.t -> clock_eff list -> subst -> clock_eff * subst -- GitLab