From 632fae4cae9df0367bdc5fc7863d145d7e8fce2e Mon Sep 17 00:00:00 2001 From: Erwan Jahier <jahier@imag.fr> Date: Mon, 30 Jun 2008 09:40:41 +0200 Subject: [PATCH] Cosmetic change: Handle predef operator clocking in a separate module PredefEvelClock, in a similar manner as for type checking. --- src/Makefile | 2 ++ src/evalClock.ml | 42 ++++++++-------------- src/predefEvalClock.ml | 71 +++++++++++++++++-------------------- src/test/test.res.exp | 80 +++++++++++++++++++++--------------------- src/unifyClock.ml | 17 ++++++++- src/unifyClock.mli | 10 +++++- 6 files changed, 115 insertions(+), 107 deletions(-) diff --git a/src/Makefile b/src/Makefile index 5b96be8e..be00b3ba 100644 --- a/src/Makefile +++ b/src/Makefile @@ -44,6 +44,8 @@ SOURCES = \ ./predefEvalType.ml \ ./predefEvalConst.mli \ ./predefEvalConst.ml \ + ./predefEvalClock.mli \ + ./predefEvalClock.ml \ ./evalConst.mli \ ./evalConst.ml \ ./evalType.mli \ diff --git a/src/evalClock.ml b/src/evalClock.ml index a46d4602..89c77482 100644 --- a/src/evalClock.ml +++ b/src/evalClock.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 26/06/2008 (at 17:36) by Erwan Jahier> *) +(** Time-stamp: <modified the 30/06/2008 (at 09:37) by Erwan Jahier> *) open Predef @@ -169,12 +169,6 @@ let (get_clock_profile : node_exp_eff -> clock_profile) = let ci2str = CompiledDataDump.string_of_clock2 -(******************************************************************************) -(* Stuff to generated fresh var clocks *) - -let var_type = ref 0 -let reset_var_type () = var_type := 0 -let get_var_type () = incr var_type; !var_type let cpt_var_name = ref 0 @@ -182,7 +176,6 @@ let (make_dummy_var: string -> Ident.t) = fun str -> 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) @@ -192,7 +185,7 @@ let concat_subst (s11,s12) (s21,s22) = (s11 @ s21, s12@s22) 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 (); + UnifyClock.reset_var_type (); (* we split f in into two so that we can reinit the fresh clock var generator *) f_aux id_solver s ve @@ -269,10 +262,7 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list | HAT_eff(i,ve) -> f_aux id_solver s ve (* nb: the args have been put inside the HAT_eff constructor *) - | Predef_eff (ICONST_n _,_) - | Predef_eff (RCONST_n _,_) - | Predef_eff (TRUE_n,_) - | Predef_eff (FALSE_n,_) -> [get_constant_clock ()],s + | IDENT_eff idref -> ( try ([var_info_eff_to_clock_eff (id_solver.id2var idref lxm)], s) with _ -> (* => it is a constant *) [get_constant_clock ()],s @@ -285,7 +275,7 @@ 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 = ClockVar (get_var_type ()) in + let rel_base = ClockVar (UnifyClock.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 @@ -309,9 +299,19 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list assert(List.length args = 1); f_aux id_solver s (List.hd args) + | Predef_eff (op,sargs) -> + let clk_args, s = f_list id_solver s args in + + let flat_clk_args = List.flatten clk_args in (* => mono-clock! *) + let clk_list = + if args = [] then [] else + let clk,s = UnifyClock.list lxm flat_clk_args s in + List.map (List.map (apply_subst s)) clk_args + in + PredefEvalClock.f op lxm sargs clk_list, s + (* may have tuples as arguments *) | TUPLE_eff - | Predef_eff (_,_) | ARROW_eff | FBY_eff | WITH_eff @@ -329,16 +329,6 @@ and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list let clk_list = match posop with | TUPLE_eff -> List.map (apply_subst s) flat_clk_args - - | Predef_eff (IF_n,[]) -> - (* for ite, the arity of the result is not the arity of - the condition *) - List.map (apply_subst s) (List.hd (List.tl clk_args)) - - | Predef_eff ((Map|Fill|Red|FillRed|BoolRed), sarg) -> - assert false - (* TODO *) - | _ -> List.map (apply_subst s) (List.hd clk_args) in clk_list, s @@ -358,5 +348,3 @@ and (eval_by_name_clock : id_solver -> by_name_op_eff -> Lxm.t -> let clk,s = UnifyClock.list lxm flat_clk_args s in let clk_list = List.map (apply_subst s) (List.hd clk_args) in clk_list, s - - diff --git a/src/predefEvalClock.ml b/src/predefEvalClock.ml index de392113..9b92826f 100644 --- a/src/predefEvalClock.ml +++ b/src/predefEvalClock.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 09/06/2008 (at 12:25) by Erwan Jahier> *) +(** Time-stamp: <modified the 30/06/2008 (at 09:33) by Erwan Jahier> *) open Predef open CompiledData @@ -12,48 +12,43 @@ exception EvalClock_error of string (** A few useful clock profiles *) -let (arity_zero_profile: clocker) = assert false -let (arity_one_profile: clocker) = - function - | [clk1] -> clk1 - | _ -> raise (EvalClock_error "a good error msg") - -let (arity_two_profile: clocker) = +let (constant_profile: clocker) = fun _ -> [UnifyClock.get_constant_clock ()] + +let (op_profile: clocker) = function - | [clk1; clk2] -> - if clk1 = clk2 then clk1 else raise (EvalClock_error "a good error msg") - | _ -> - raise (EvalClock_error "a good error msg") + | clk::_ -> clk + | [] -> assert false -let if_clock_profile c = assert false -let fillred_clock_profile c = assert false -let map_clock_profile c = assert false -let boolred_clock_profile c = assert false +let if_clock_profile lxm sargs = + function + | [clk1; clk2; clk3] -> clk2 + | _ -> assert false + + +let fillred_clock_profile lxm sargs = assert false +let map_clock_profile lxm sargs = assert false +let boolred_clock_profile lxm sargs = assert false (* This table contains the clock profile of predefined operators *) let (f: op -> Lxm.t -> CompiledData.static_arg_eff list -> clocker) = - fun op lxm sargs -> assert false -(* match op with *) -(* | TRUE_n | FALSE_n | ICONST_n _id | RCONST_n _id *) -(* -> arity_zero_profile *) -(* *) -(* | NOT_n | REAL2INT_n | INT2REAL_n | UMINUS_n | IUMINUS_n | RUMINUS_n *) -(* -> arity_one_profile *) -(* *) -(* *) -(* | IMPL_n | AND_n | OR_n | XOR_n *) -(* | NEQ_n | EQ_n | LT_n | LTE_n | GT_n | GTE_n *) -(* | MINUS_n | PLUS_n | TIMES_n | SLASH_n *) -(* | RMINUS_n | RPLUS_n | RTIMES_n | RSLASH_n *) -(* | DIV_n | MOD_n | IMINUS_n | IPLUS_n | ISLASH_n | ITIMES_n *) -(* -> arity_two_profile *) -(* *) -(* | IF_n -> if_clock_profile *) -(* | Red | Fill | FillRed -> fillred_clock_profile lxm sargs *) -(* | Map -> map_clock__profile lxm sargs *) -(* | BoolRed -> boolred_clock__profile lxm sargs *) -(* *) -(* | NOR_n | DIESE_n -> assert false *) + fun op lxm sargs -> + match op with + | TRUE_n | FALSE_n | ICONST_n _ | RCONST_n _ -> constant_profile + + | NOT_n | REAL2INT_n | INT2REAL_n | UMINUS_n | IUMINUS_n | RUMINUS_n + | IMPL_n | AND_n | OR_n | XOR_n + | NEQ_n | EQ_n | LT_n | LTE_n | GT_n | GTE_n + | MINUS_n | PLUS_n | TIMES_n | SLASH_n + | RMINUS_n | RPLUS_n | RTIMES_n | RSLASH_n + | DIV_n | MOD_n | IMINUS_n | IPLUS_n | ISLASH_n | ITIMES_n + | NOR_n | DIESE_n + -> op_profile + + | IF_n -> if_clock_profile lxm sargs + | Red | Fill | FillRed -> fillred_clock_profile lxm sargs + | Map -> map_clock_profile lxm sargs + | BoolRed -> boolred_clock_profile lxm sargs + diff --git a/src/test/test.res.exp b/src/test/test.res.exp index 579b081f..e2684be0 100644 --- a/src/test/test.res.exp +++ b/src/test/test.res.exp @@ -29,7 +29,7 @@ let tel -- end of node Int8::fulladd -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/NONREG/Int.lus ---------------------------------------------------------------------- @@ -1092,7 +1092,7 @@ returns ( c:bool when b; d:bool when c); -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 31, column 38 *** when compiling lustre program should_work/NONREG/clock.lus ---------------------------------------------------------------------- @@ -3840,7 +3840,7 @@ let tel -- end of node Gyroscope2::TooFar -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/demo/Gyroscope2.lus ---------------------------------------------------------------------- @@ -3876,14 +3876,14 @@ let tel -- end of node alias::aliasPredefNot -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34 *** when compiling lustre program should_work/demo/alias.lus ---------------------------------------------------------------------- ====> ../lus2lic -vl 2 --compile-all-items should_work/demo/bred.lus Opening file /home/jahier/lus2lic/src/test/should_work/demo/bred.lus -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 31, column 38 *** when compiling lustre program should_work/demo/bred.lus ---------------------------------------------------------------------- @@ -3891,7 +3891,7 @@ Opening file /home/jahier/lus2lic/src/test/should_work/demo/bred.lus Opening file /home/jahier/lus2lic/src/test/should_work/demo/bred_lv4.lus type bred_lv4::T1_ARRAY = bool^2; -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 31, column 38 *** when compiling lustre program should_work/demo/bred_lv4.lus ---------------------------------------------------------------------- @@ -4127,7 +4127,7 @@ let tel -- end of node filliter::copie -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/demo/filliter.lus ---------------------------------------------------------------------- @@ -4244,7 +4244,7 @@ let tel -- end of node map_red_iter::traite_genCore_itere -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/demo/map_red_iter.lus ---------------------------------------------------------------------- @@ -4260,7 +4260,7 @@ let tel -- end of node mapdeRed::incr -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/demo/mapdeRed.lus ---------------------------------------------------------------------- @@ -4272,7 +4272,7 @@ let tel -- end of node mapiter::incr_tab -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34 *** when compiling lustre program should_work/demo/mapiter.lus ---------------------------------------------------------------------- @@ -4282,14 +4282,14 @@ const mappredef::N = 3; type mappredef::tab_int = int^3; type mappredef::tab_bool = bool^3; -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34 *** when compiling lustre program should_work/demo/mappredef.lus ---------------------------------------------------------------------- ====> ../lus2lic -vl 2 --compile-all-items should_work/demo/plus.lus Opening file /home/jahier/lus2lic/src/test/should_work/demo/plus.lus -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 31, column 38 *** when compiling lustre program should_work/demo/plus.lus ---------------------------------------------------------------------- @@ -4310,7 +4310,7 @@ let tel -- end of node rediter::max -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/demo/rediter.lus ---------------------------------------------------------------------- @@ -4322,7 +4322,7 @@ let tel -- end of node redoptest::max -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/demo/redoptest.lus ---------------------------------------------------------------------- @@ -4462,7 +4462,7 @@ let tel -- end of node iter::filled -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/fab_test/iter.lus ---------------------------------------------------------------------- @@ -4481,7 +4481,7 @@ let tel -- end of node iterate::mapped -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34 *** when compiling lustre program should_work/fab_test/iterate.lus ---------------------------------------------------------------------- @@ -5965,7 +5965,7 @@ let tel -- end of node FillFollowedByRed::filled -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/FillFollowedByRed.lus ---------------------------------------------------------------------- @@ -6027,7 +6027,7 @@ let tel -- end of node Gyroscope::TooFar -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/Gyroscope.lus ---------------------------------------------------------------------- @@ -6052,7 +6052,7 @@ let tel -- end of node produitBool::iterated_isElementOf_ -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/ProduitBool/produitBool.lus ---------------------------------------------------------------------- @@ -6084,7 +6084,7 @@ let tel -- end of node shiftFill_ludic::n_selectOneStage -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/ProduitBool/shiftFill_ludic.lus ---------------------------------------------------------------------- @@ -6117,7 +6117,7 @@ let tel -- end of node shift_ludic::n_selectOneStage -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/ProduitBool/shift_ludic.lus ---------------------------------------------------------------------- @@ -6137,7 +6137,7 @@ let tel -- end of node arrays::incr -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/arrays.lus ---------------------------------------------------------------------- @@ -6179,7 +6179,7 @@ let tel -- end of node calculs_max::fill_bool -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/calculs_max.lus ---------------------------------------------------------------------- @@ -6213,7 +6213,7 @@ let tel -- end of node deSimone::prop1_iter -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/deSimone.lus ---------------------------------------------------------------------- @@ -6227,7 +6227,7 @@ let tel -- end of node iterFibo::fibo -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/iterFibo.lus ---------------------------------------------------------------------- @@ -6259,7 +6259,7 @@ let tel -- end of node mapiter::fill_bitalt -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/mapiter.lus ---------------------------------------------------------------------- @@ -6275,7 +6275,7 @@ let tel -- end of node matrice::fibo -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/matrice.lus ---------------------------------------------------------------------- @@ -6284,7 +6284,7 @@ Opening file /home/jahier/lus2lic/src/test/should_work/lionel/matrice2.lus const matrice2::m = 2; const matrice2::n = 2; -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/matrice2.lus ---------------------------------------------------------------------- @@ -6293,7 +6293,7 @@ Opening file /home/jahier/lus2lic/src/test/should_work/lionel/minus.lus const minus::m = 2; const minus::n = 3; -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34 *** when compiling lustre program should_work/lionel/minus.lus ---------------------------------------------------------------------- @@ -6313,7 +6313,7 @@ let tel -- end of node moyenne::moyenne_step -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/moyenne.lus ---------------------------------------------------------------------- @@ -6348,7 +6348,7 @@ let tel -- end of node normal::int2InfoChgIndiv -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34 *** when compiling lustre program should_work/lionel/normal.lus ---------------------------------------------------------------------- @@ -6368,7 +6368,7 @@ let tel -- end of node pipeline::oneStep_pipe -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/pipeline.lus ---------------------------------------------------------------------- @@ -6392,7 +6392,7 @@ let tel -- end of node predefOp::bitalt -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/predefOp.lus ---------------------------------------------------------------------- @@ -6404,7 +6404,7 @@ let tel -- end of node redIf::monIf -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/redIf.lus ---------------------------------------------------------------------- @@ -6413,7 +6413,7 @@ Opening file /home/jahier/lus2lic/src/test/should_work/lionel/simpleRed.lus const simpleRed::m = 3; const simpleRed::n = 2; -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/simpleRed.lus ---------------------------------------------------------------------- @@ -6450,7 +6450,7 @@ let tel -- end of node testSilus::int2InfoChgIndiv -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34 *** when compiling lustre program should_work/lionel/testSilus.lus ---------------------------------------------------------------------- @@ -6481,7 +6481,7 @@ let tel -- end of node triSel::minFromRank -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/lionel/triSel.lus ---------------------------------------------------------------------- @@ -6530,7 +6530,7 @@ let tel -- end of node contractForElementSelectionInArray::selectOneStage -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/packEnvTest/contractForElementSelectionInArray/contractForElementSelectionInArray.lus ---------------------------------------------------------------------- @@ -6569,7 +6569,7 @@ let tel -- end of node intArray::iterated_isElementOf_ -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/packEnvTest/contractForElementSelectionInArray/main.lus ---------------------------------------------------------------------- @@ -6617,7 +6617,7 @@ let tel -- end of node tri::minFromRank -*** oops: an internal error occurred in file evalClock.ml, line 344, column 4 +*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38 *** when compiling lustre program should_work/packEnvTest/contractForElementSelectionInArray/tri.lus ---------------------------------------------------------------------- diff --git a/src/unifyClock.ml b/src/unifyClock.ml index 93496085..e62009f3 100644 --- a/src/unifyClock.ml +++ b/src/unifyClock.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 26/06/2008 (at 16:58) by Erwan Jahier> *) +(** Time-stamp: <modified the 30/06/2008 (at 09:39) by Erwan Jahier> *) open SyntaxTree @@ -18,6 +18,21 @@ type subst = (Ident.t * Ident.t) list * (int * clock_eff) list (* exported *) let (empty_subst:subst) = [],[] +(******************************************************************************) +(* Stuff to generate fresh var clocks *) + +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 diff --git a/src/unifyClock.mli b/src/unifyClock.mli index 14a28162..d129a35f 100644 --- a/src/unifyClock.mli +++ b/src/unifyClock.mli @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 26/06/2008 (at 16:58) by Erwan Jahier> *) +(** Time-stamp: <modified the 26/06/2008 (at 17:53) by Erwan Jahier> *) open CompiledData @@ -35,3 +35,11 @@ val apply_subst:subst -> clock_eff -> clock_eff (** 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 + + +(* Stuff to generated fresh var clocks + XXX bad place, bad name +*) +val reset_var_type : unit -> unit +val get_constant_clock : unit -> clock_eff +val get_var_type : unit -> int -- GitLab