diff --git a/lv6-ref-man/Makefile b/lv6-ref-man/Makefile
index 8073c58f0af91eb98fdd5c8a569b17b5fa16c14a..902b1e6cedbead4f32136a9d9fb6fa0f7315a055 100644
--- a/lv6-ref-man/Makefile
+++ b/lv6-ref-man/Makefile
@@ -17,13 +17,23 @@ SRCS= \
preambule.tex \
touch.tex
+FIGS=\
+ $(OBJPDF)/patate.tex \
+ $(OBJPDF)/edge.tex \
+ $(OBJPDF)/df.tex \
+ $(OBJPDF)/map1.tex \
+ $(OBJPDF)/red1.tex \
+ $(OBJPDF)/fill1.tex \
+ $(OBJPDF)/fillred1.tex
+
# Les inclusions de figures
FIGDIR=figs
-all: $(OBJPDF) \
- $(FIGS) \
- $(MAIN).pdf
+all: $(FIGS) $(OBJPDF) $(MAIN).pdf
+
+.PHONY: dofigs
+dofigs: $(FIGS)
$(OBJPDF) :
mkdir $(OBJPDF)
@@ -88,14 +98,6 @@ EXEMPLES= \
$(LUSTRE_DIR)/packEnvTest/complex.lus\
$(LUSTRE_DIR)/packEnvTest/model.lus
-FIGS=\
- $(OBJPDF)/patate.tex \
- $(OBJPDF)/edge.tex \
- $(OBJPDF)/df.tex \
- $(OBJPDF)/map1.tex \
- $(OBJPDF)/red1.tex \
- $(OBJPDF)/fill1.tex \
- $(OBJPDF)/fillred1.tex
lus2tex:
for f in ${EXEMPLES}; do \
diff --git a/lv6-ref-man/lv6-ref-man.tex b/lv6-ref-man/lv6-ref-man.tex
index 4425aac61ef1f6858264ea3805fd470b949f5600..ec3a277df414ecbc71217e0219039a75eeeffccf 100644
--- a/lv6-ref-man/lv6-ref-man.tex
+++ b/lv6-ref-man/lv6-ref-man.tex
@@ -892,12 +892,12 @@ sense that they are operating pointwise on streams.
\sxDef{Expression\_List} \is \sx{Expression} \sor
\sx{Expression} \lx{,} \sx{Expression\_List}
\\
-\sxDef{Record\_Exp} \is \lx{$\{$} \sx{Field\_Exp\_List} \lx{$\}$}
+\sxDef{Record\_Exp} \is \sx{Ident} \lx{$\{$} \sx{Field\_Exp\_List} \lx{$\}$}
\\
\sxDef{Field\_Exp\_List} \is \sx{Field\_Exp} \sor
\sx{Field\_Exp} \lx{;} \sx{Field\_Exp\_List}
\\
-\sxDef{Field\_Exp} \is \sx{Ident} \lx{:} \sx{Expression}
+\sxDef{Field\_Exp} \is \sx{Ident} \lx{=} \sx{Expression}
\\
\sxDef{Array\_Exp} \is \lx{[} \sx{Expression\_List} \lx{]}
\sor \sx{Expression} \lx{\^{~}} \sx{Expression}
diff --git a/src/TODO b/src/TODO
index b22bf8a7c6761a1ca99dc73b847d31f0f9ddc70c..018a9cf7c159e64525b3aa5ea2fbdcf6709d18af 100644
--- a/src/TODO
+++ b/src/TODO
@@ -122,6 +122,9 @@ n'est pas le cas pour l'instant... cf [solve_ident]
-----------------------------------------------------------------------
A faire
+* Attacher le type et l'horloge des expressions aux expressions elle-meme,
+plutot que d'utiliser une hashtbl
+
* Ne pas générer de "current", "->", "pre" (i.e., les traduire en
termes de "merge" et "fby").
diff --git a/src/evalClock.ml b/src/evalClock.ml
index 941498b4f21034d79a764adf61aba355f85da76e..870f6685ff0cd056af21c365ca83e4b3ea9706bc 100644
--- a/src/evalClock.ml
+++ b/src/evalClock.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 04/03/2009 (at 11:02) by Erwan Jahier> *)
+(** Time-stamp: <modified the 09/03/2009 (at 16:11) by Erwan Jahier> *)
open Predef
@@ -145,34 +145,26 @@ let (check_res : Lxm.t -> subst -> Eff.left list -> Eff.id_clock 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))
- If it is a sub_clock, we return the accumulator (the current substitutions)
+ If it is a sub_clock, we return the accumulator (the current substitution)
*)
-let rec (is_a_sub_clock : Lxm.t -> subst -> Eff.id_clock -> Eff.id_clock ->
- subst option) =
+let rec (is_a_sub_clock :
+ Lxm.t -> subst -> Eff.id_clock -> Eff.id_clock -> subst option) =
fun lxm s (id_sc,sc) (id_c,c) ->
- (* check if [sc] is a sub-clock of [c] (in the large
- sense). Returns Some updated substitution if it is the case,
- and None otherwise *)
+ (* Check if [sc] is a sub-clock of [c] (in the large sense).
+ Returns Some updated substitution if it is the case, and None otherwise *)
let rec aux sc c =
match sc, c with
(* the base clock is a sub-clock of all clocks *)
- | BaseEff, (BaseEff|On(_,_)|ClockVar _) -> Some s
-
+ | BaseEff, (BaseEff|On(_,_)|ClockVar _) -> Some s
| On(_,_), BaseEff -> None
- | On(_), On(_,c_clk) -> (
+
+ | sc, On(_,c_clk) -> (
try Some(UnifyClock.f lxm s sc c)
- with _ -> aux sc c_clk
+ with Compile_error _ -> aux sc c_clk
)
- | ClockVar j, BaseEff -> Some(UnifyClock.f lxm s sc c)
-
- | ClockVar i, On(_,_)
- | ClockVar i, ClockVar _ ->
- let s1,s2 = s in
- Some (s1,(i,c)::s2)
-
- | On(_,_), ClockVar i ->
- let s1,s2 = s in
- Some (s1,(i,sc)::s2)
+ | _,_ ->
+ try Some(UnifyClock.f lxm s sc c)
+ with Compile_error _ -> None
in
aux sc c
@@ -196,31 +188,39 @@ let val_exp_eff_clk_tab:(Eff.val_exp, Eff.id_clock list) Hashtbl.t = Hashtbl.cre
let tabulate_res vef clock_eff_list =
(* print_string "*** '"; *)
(* print_string (LicDump.string_of_val_exp_eff vef); *)
-(* print_string "' -> "; *)
-(* print_string (String.concat "," (List.map LicDump.string_of_clock2 clock_eff_list)); *)
-(* print_string "\n"; *)
-(* flush stdout; *)
- Hashtbl.add val_exp_eff_clk_tab vef clock_eff_list
-
-let (add : Eff.val_exp -> Eff.id_clock list -> unit) =
- fun ve cl ->
- Hashtbl.add val_exp_eff_clk_tab ve cl
+(* let lxm = match vef with *)
+(* |CallByPosEff(op,_) -> op.src *)
+(* | CallByNameEff(op,_) -> op.src *)
+(* in *)
+(* print_string (Lxm.details lxm); *)
+(* print_string "' -> "; *)
+(* print_string (String.concat "," *)
+(* (List.map (fun (_,clk) -> LicDump.string_of_clock2 clk) *)
+(* clock_eff_list)); *)
+(* print_string "\n"; *)
+(* flush stdout; *)
+
+ Hashtbl.replace val_exp_eff_clk_tab vef clock_eff_list
+
+let (add : Eff.val_exp -> Eff.id_clock list -> unit) = tabulate_res
+(* fun ve cl -> *)
+(* Hashtbl.add val_exp_eff_clk_tab ve cl *)
let (lookup : Eff.val_exp -> Eff.id_clock list) =
fun vef ->
try
let res = Hashtbl.find val_exp_eff_clk_tab vef in
- let rec var_clock_to_base = function
- (* Some expressions migth be infered to be a variable clock
- (e.g., constants). In that case, it is ok to consider that such
- expressions are on the base clock at top-level.
- *)
- | BaseEff -> BaseEff
- | ClockVar _ -> BaseEff
- | On(v, clk) -> On(v, var_clock_to_base clk)
- in
- List.map (fun (id,clk) -> id, var_clock_to_base clk) res
- with _ ->
+(* let rec var_clock_to_base = function *)
+(* (* Some expressions migth be infered to be a variable clock *)
+(* (e.g., constants). In that case, it is ok to consider that such *)
+(* expressions are on the base clock in the end (i.e., at top-level). *)
+(* *) *)
+(* | BaseEff -> BaseEff *)
+(* | ClockVar i -> BaseEff *)
+(* | On(v, clk) -> On(v, var_clock_to_base clk) *)
+(* in *)
+ List.map (fun (id,clk) -> id, (* var_clock_to_base *) clk) res
+ with Not_found ->
print_string "*** No entry in clock table for the expression '";
print_string (LicDump.string_of_val_exp_eff vef);
print_string "'\n ";
@@ -229,29 +229,58 @@ let (lookup : Eff.val_exp -> Eff.id_clock list) =
let (copy : Eff.val_exp -> Eff.val_exp -> unit) =
fun ve1 ve2 ->
- let tl = try lookup ve2 with _ -> assert false in
+ let tl = lookup ve2 in
Hashtbl.add val_exp_eff_clk_tab ve1 tl
(******************************************************************************)
(** Now we can go on and define [f]. *)
-let cpt_var_name = ref 0
-let rec (f : Eff.id_solver -> subst -> Eff.val_exp -> Eff.id_clock list * subst) =
- fun id_solver s ve ->
- cpt_var_name := 0;
- UnifyClock.reset_var_type ();
+(* During the inner call to f_aux, some intermediary clock variables
+ may remain. This function tries to get rid of them using s *)
+let apply_subst_to_clk_tbl s =
+ Hashtbl.iter
+ (fun ve cel ->
+ let cel2 =
+ List.map
+ (fun (id,clk) ->
+ let clk = apply_subst2 s clk in
+ id, clk)
+ cel
+ in
+ if cel <> cel2 then (
+(* let lxm = match ve with *)
+(* |CallByPosEff(op,_) -> op.src *)
+(* | CallByNameEff(op,_) -> op.src *)
+(* in *)
+(* print_string ("*** Replacing the clock of " ^ *)
+(* (string_of_val_exp_eff ve) ^ " [" ^(Lxm.position lxm) *)
+(* ^ "] (which was bound to " ^ *)
+(* (String.concat "," *)
+(* (List.map (fun (_,clk) -> string_of_clock2 clk) cel))^ *)
+(* ") by " ^ *)
+(* (String.concat "," *)
+(* (List.map (fun (_,clk) -> string_of_clock2 clk) cel2))^ *)
+(* "\n"); *)
+(* flush stdout; *)
+ Hashtbl.replace val_exp_eff_clk_tab ve cel2
+ );
+ )
+ val_exp_eff_clk_tab
+
+let rec (f : Lxm.t -> Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list ->
+ Eff.id_clock list * subst) =
+ fun lxm id_solver s ve exp_clks ->
(* we split f so that we can reinit the fresh clock var generator *)
- let res = f_aux id_solver s ve in
- let s = snd res in
- (* during the inner call to f_aux, some intermediary clock variables
- may remain. *)
- Hashtbl.iter
- (fun ve cel ->
- let cel2 = List.map (fun (id,clk) -> id, apply_subst2 s clk) cel in
- if cel <> cel2 then
- Hashtbl.replace val_exp_eff_clk_tab ve cel2)
- val_exp_eff_clk_tab;
- res
+ let inf_clks, s = f_aux id_solver s ve in
+ let s = List.fold_left2
+ (fun s eclk iclk -> UnifyClock.f lxm s eclk iclk)
+ s
+ exp_clks
+ (List.map (fun (_,clk) -> clk) inf_clks)
+ in
+ apply_subst_to_clk_tbl s;
+ inf_clks, s
+
and f_aux id_solver s ve =
@@ -269,7 +298,8 @@ and f_aux id_solver s ve =
cel, s
(* iterate f on a list of expressions *)
-and (f_list : Eff.id_solver -> subst -> Eff.val_exp list -> Eff.id_clock list list * subst) =
+and (f_list : Eff.id_solver -> subst -> Eff.val_exp list ->
+ Eff.id_clock list list * subst) =
fun id_solver s args ->
let aux (acc,s) arg =
let cil, s = f_aux id_solver s arg in
@@ -277,6 +307,7 @@ and (f_list : Eff.id_solver -> subst -> Eff.val_exp list -> Eff.id_clock list li
in
let (cil, s) = List.fold_left aux ([],s) args in
let cil = List.rev cil in
+ apply_subst_to_clk_tbl s;
cil, s
and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp list ->
@@ -286,7 +317,7 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp
match posop,args with
| Eff.CURRENT,args -> ( (* we return the clock of the argument *)
let clocks_of_args, s = f_list id_solver s args in
- let current_clock = function
+ let current_clock = function
| (id, BaseEff) -> (id, BaseEff)
| (id, On(_,clk)) -> (id, clk)
| (_, ClockVar _) -> assert false
@@ -294,7 +325,7 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp
List.map current_clock (List.flatten clocks_of_args), s
)
| Eff.WHEN clk_exp,args -> (
- let c_clk, when_exp_clk =
+ let c_clk, when_exp_clk =
match clk_exp with
| Base -> BaseEff, BaseEff
| NamedClock { it = (cc,c) ; src = lxm } ->
@@ -328,7 +359,8 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp
| id, ClockVar i ->
let id_when_exp_clk = id, when_exp_clk in
let (s1,s2) = s in
- id_when_exp_clk, (s1,(i,when_exp_clk)::s2)
+ id_when_exp_clk,
+ (s1, UnifyClock.add_subst2 i when_exp_clk s2)
in
id_when_exp_clk, s
in
@@ -366,12 +398,13 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp
| Eff.IDENT idref,args -> (
try ([var_info_eff_to_clock_eff (id_solver.id2var idref lxm)], s)
- with _ -> (* => it is a constant *)
- [Ident.of_idref idref, get_constant_clock ()], s
+ with Compile_error _ -> (* => it is a constant *)
+ let s, clk = UnifyClock.new_clock_var s in
+ [Ident.of_idref idref, clk], s
)
| Eff.CALL node_exp_eff,args ->
let (cil_arg, cil_res) = get_clock_profile node_exp_eff.it in
- let rel_base = ClockVar (UnifyClock.get_var_type ()) in
+ let s, rel_base = UnifyClock.new_clock_var s in
(* the value of the base clock of a node is actually relative
to the context into which the node is called.
@@ -413,7 +446,7 @@ and (eval_by_pos_clock : Eff.id_solver -> Eff.by_pos_op -> Lxm.t -> Eff.val_exp
let _clk,s = UnifyClock.list lxm flat_clk_args s in
List.map (List.map (apply_subst s)) clk_args, s
in
- PredefEvalClock.f op lxm sargs clk_list, s
+ PredefEvalClock.f op lxm sargs s clk_list
(* may have tuples as arguments *)
| Eff.TUPLE,args
diff --git a/src/evalClock.mli b/src/evalClock.mli
index 88e1a050e8f3085fa01a6734682c2fa5ee7228c1..6de003551ce30daf59e5f4c3c553c4b1e47105b0 100644
--- a/src/evalClock.mli
+++ b/src/evalClock.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 28/01/2009 (at 14:43) by Erwan Jahier> *)
+(** Time-stamp: <modified the 05/03/2009 (at 10:16) by Erwan Jahier> *)
open UnifyClock
@@ -7,7 +7,8 @@ open UnifyClock
and returns a clock profile that contains all the necessary information
to be able to check.
*)
-val f : Eff.id_solver -> subst -> Eff.val_exp -> Eff.id_clock list * subst
+val f : Lxm.t -> Eff.id_solver -> subst -> Eff.val_exp -> Eff.clock list ->
+ Eff.id_clock list * subst
(** [check_res lxm cel cil] checks that the expected output clock
diff --git a/src/getEff.ml b/src/getEff.ml
index 5c626e9c51b49b437d100e07816660cf22082dab..ce9a8ef531bbdc3acb4d287a0ae44cf60b6623f5 100644
--- a/src/getEff.ml
+++ b/src/getEff.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 03/03/2009 (at 17:18) by Erwan Jahier> *)
+(** Time-stamp: <modified the 05/03/2009 (at 10:11) by Erwan Jahier> *)
open Lxm
@@ -95,7 +95,10 @@ and (type_check_equation: Eff.id_solver -> Lxm.t -> Eff.left list ->
and (clock_check_equation:Eff.id_solver -> Lxm.t -> Eff.left list ->
Eff.val_exp -> unit) =
fun id_solver lxm lpl_eff ve_eff ->
- let right_part,s = EvalClock.f id_solver UnifyClock.empty_subst ve_eff in
+ let clk_list = List.map Eff.clock_of_left lpl_eff in
+ let right_part,s =
+ EvalClock.f lxm id_solver UnifyClock.empty_subst ve_eff clk_list
+ in
EvalClock.check_res lxm s lpl_eff right_part
@@ -741,7 +744,7 @@ let (assertion : Eff.id_solver -> SyntaxTreeCore.val_exp Lxm.srcflagged ->
(* Clock check the assertion*)
let clock_eff_list, _s =
- EvalClock.f id_solver UnifyClock.empty_subst val_exp_eff
+ EvalClock.f vef.src id_solver UnifyClock.empty_subst val_exp_eff [BaseEff]
in
match clock_eff_list with
| [id, BaseEff]
diff --git a/src/inline.ml b/src/inline.ml
index c3891f4528d45d5dc7fc0c24b2f5f40f1d861908..efedf909993764264b727fbe40eb2326a9ade62a 100644
--- a/src/inline.ml
+++ b/src/inline.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 04/02/2009 (at 15:27) by Erwan Jahier> *)
+(** Time-stamp: <modified the 06/03/2009 (at 17:51) by Erwan Jahier> *)
open Lxm
@@ -46,18 +46,14 @@ let rec (list_map3:
let (check_clock_and_type :
Eff.id_solver -> Lxm.t -> val_exp -> Eff.type_ -> Eff.id_clock -> unit) =
- fun id_solver lxm rhs exp_type exp_clock ->
+ fun id_solver lxm rhs exp_type (_,exp_clock) ->
(* Let's be paranoiac and check types and clocks of the expression
this function generates.
Moreover, this fills some tables that may be used by
the call to Split.eq below....*)
if (EvalType.f id_solver rhs <> [exp_type]) then assert false;
- try
- let (clock, subst) =
- EvalClock.f id_solver UnifyClock.empty_subst rhs
- in
- ignore(UnifyClock.f lxm subst (snd(List.hd clock)) (snd exp_clock));
+ try ignore(EvalClock.f lxm id_solver UnifyClock.empty_subst rhs [exp_clock])
with _ -> assert false
(********************************************************************************)
diff --git a/src/licDump.ml b/src/licDump.ml
index f5c5759b20754f891a2b816ffdba44a22b808529..baf9d40fcff31feb689f9ef581af71159832609c 100644
--- a/src/licDump.ml
+++ b/src/licDump.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 04/03/2009 (at 15:05) by Erwan Jahier> *)
+(** Time-stamp: <modified the 06/03/2009 (at 16:26) by Erwan Jahier> *)
open Printf
open Lxm
@@ -320,7 +320,8 @@ and (string_of_by_pos_op_eff: Eff.by_pos_op srcflagged -> Eff.val_exp list -> st
match op with
| Predef.ICONST_n _ | Predef.RCONST_n _ | Predef.NOT_n
| Predef.UMINUS_n | Predef.IUMINUS_n | Predef.RUMINUS_n
- | Predef.FALSE_n | Predef.TRUE_n -> tuple vel
+ | Predef.FALSE_n | Predef.TRUE_n ->
+ tuple vel
| _ -> tuple_par vel
else
"<<" ^
@@ -643,7 +644,10 @@ and string_of_clock (ck : Eff.clock) =
| On(clk_exp,_) ->
let clk_exp_str = string_of_ident_clk clk_exp in
" when " ^ clk_exp_str
- | ClockVar _ -> assert false
+ | ClockVar _ ->
+ "" (* it migth occur that (unused) constant remain with a clock var.
+ But in that case, it is ok to consider then as on the base clock.
+ *)
(* | ClockVar i -> "_clock_var_" ^ (string_of_int i) *)
and op2string = Predef.op2string
diff --git a/src/predefEvalClock.ml b/src/predefEvalClock.ml
index 8c3fbd46068fd35c31db37ef80af890ec05572b4..6c91c7b82165679b75865f7228ec17b0c56995c2 100644
--- a/src/predefEvalClock.ml
+++ b/src/predefEvalClock.ml
@@ -1,56 +1,61 @@
-(** Time-stamp: <modified the 11/09/2008 (at 16:15) by Erwan Jahier> *)
+(** Time-stamp: <modified the 06/03/2009 (at 14:22) by Erwan Jahier> *)
open Predef
-(* exported *)
-type clocker = Eff.id_clock Predef.evaluator
(* exported *)
exception EvalClock_error of string
+type clocker = UnifyClock.subst -> Eff.id_clock list list ->
+ Eff.id_clock list * UnifyClock.subst
+
+
(** A few useful clock profiles *)
let (constant_profile: string -> clocker) =
- fun str _ -> [Ident.of_string str, UnifyClock.get_constant_clock ()]
+ fun str s _ ->
+ let s, clk = UnifyClock.new_clock_var s in
+ [Ident.of_string str, clk], s
let (op_profile: clocker) =
- function
- | clk::_ -> clk
- | [] -> assert false
+ fun s cl ->
+ match cl with
+ | clk::_ -> clk, s
+ | [] -> assert false
-let if_clock_profile lxm sargs =
+let if_clock_profile lxm sargs s =
function
- | [clk1; clk2; clk3] -> clk2
+ | [clk1; clk2; clk3] -> clk2, s
| _ -> assert false
let rec fill x n = if n > 0 then (x::(fill x (n-1))) else []
-let fillred_clock_profile lxm sargs clks =
+let fillred_clock_profile lxm sargs s clks =
let (_, lto) = PredefEvalType.fillred_profile lxm sargs in
let clks = List.flatten clks in
- fill (List.hd clks) (List.length lto)
+ fill (List.hd clks) (List.length lto), s
-let map_clock_profile lxm sargs clks =
+let map_clock_profile lxm sargs s clks =
let (_, lto) = PredefEvalType.map_profile lxm sargs in
let clks = List.flatten clks in
- fill (List.hd clks) (List.length lto)
+ fill (List.hd clks) (List.length lto), s
-let boolred_clock_profile lxm sargs clks =
+let boolred_clock_profile lxm sargs s clks =
let (_, lto) = PredefEvalType.boolred_profile lxm sargs in
let clks = List.flatten clks in
- fill (List.hd clks) (List.length lto)
+ fill (List.hd clks) (List.length lto), s
(* This table contains the clock profile of predefined operators *)
let (f: op -> Lxm.t -> Eff.static_arg list -> clocker) =
- fun op lxm sargs ->
+ fun op lxm sargs s ->
match op with
| TRUE_n | FALSE_n | ICONST_n _ | RCONST_n _ ->
- constant_profile (Predef.op2string op)
+ constant_profile (Predef.op2string op) s
| NOT_n | REAL2INT_n | INT2REAL_n | UMINUS_n | IUMINUS_n | RUMINUS_n
| IMPL_n | AND_n | OR_n | XOR_n
@@ -59,12 +64,12 @@ let (f: op -> Lxm.t -> Eff.static_arg list -> clocker) =
| 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
+ -> op_profile s
- | 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
+ | IF_n -> if_clock_profile lxm sargs s
+ | Red | Fill | FillRed -> fillred_clock_profile lxm sargs s
+ | Map -> map_clock_profile lxm sargs s
+ | BoolRed -> boolred_clock_profile lxm sargs s
diff --git a/src/predefEvalClock.mli b/src/predefEvalClock.mli
index e9406afc0b1d5c4744ba1a85db12b3e500c00863..0cf63d80854b6bd7e424e09d94e050afe8d0c471 100644
--- a/src/predefEvalClock.mli
+++ b/src/predefEvalClock.mli
@@ -1,8 +1,9 @@
-(** Time-stamp: <modified the 11/09/2008 (at 16:12) by Erwan Jahier> *)
-
-type clocker = Eff.id_clock Predef.evaluator
+(** Time-stamp: <modified the 06/03/2009 (at 14:18) by Erwan Jahier> *)
exception EvalClock_error of string
+type clocker = UnifyClock.subst -> Eff.id_clock list list ->
+ Eff.id_clock list * UnifyClock.subst
+
val f: Predef.op -> Lxm.t -> Eff.static_arg list -> clocker
diff --git a/src/split.ml b/src/split.ml
index 92b0b9738ddf1e47bc2c14059649b8a2d649a4ca..632d60d11f67be531c614875caf829351f7a76c9 100644
--- a/src/split.ml
+++ b/src/split.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 24/02/2009 (at 14:57) by Erwan Jahier> *)
+(** Time-stamp: <modified the 06/03/2009 (at 16:41) by Erwan Jahier> *)
open Lxm
@@ -126,7 +126,7 @@ type split_acc = (Eff.eq_info srcflagged) list * Eff.var_info list
(* exported *)
let rec (eq : Eff.local_env -> Eff.eq_info Lxm.srcflagged -> split_acc) =
fun node_env { src = lxm_eq ; it = (lhs, rhs) } ->
- let n_rhs, (neqs, nlocs) = split_val_exp true node_env rhs in
+ let n_rhs, (neqs, nlocs) = split_val_exp false true node_env rhs in
{ src = lxm_eq ; it = (lhs, n_rhs) }::neqs, nlocs
and (split_eq_acc :
@@ -135,23 +135,49 @@ and (split_eq_acc :
let (neqs, nlocs) = eq node_env equation in
(split_tuples (eqs@neqs), locs@nlocs)
-and (split_val_exp : bool -> Eff.local_env -> Eff.val_exp -> Eff.val_exp * split_acc) =
- fun top_level node_env ve ->
+and (split_val_exp : bool -> bool -> Eff.local_env -> Eff.val_exp ->
+ Eff.val_exp * split_acc) =
+ fun when_flag top_level node_env ve ->
+ (* when_flag is true is the call is made from a "when" statement.
+ We need this flag in order to know if it is necessary to add
+ a when on constants. Indeed, in Lustre, it is not necessary
+ to write " 1 when clk + x " if x in on clk (its more sweet).
+ So we need to add it (because if we split "1+1+x", then it
+ is hard to know the "1" are on the clock of x).
+
+ But is is not forbidden either! so we need to make sure that there
+ is no "when"...
+
+
+ *)
match ve with
- | CallByPosEff({it=Eff.IDENT _}, _)
- | CallByPosEff({it=Eff.Predef(Predef.TRUE_n,_)}, _)
- | CallByPosEff({it=Eff.Predef(Predef.FALSE_n,_)}, _)
- | CallByPosEff({it=Eff.Predef(Predef.ICONST_n _,_)}, _)
- | CallByPosEff({it=Eff.Predef(Predef.RCONST_n _,_)}, _)
- (* We do not create an intermediary variable for those *)
- -> ve, ([],[])
+ | CallByPosEff({it=Eff.IDENT _}, _) -> ve, ([],[])
+
+ | CallByPosEff({src=lxm;it=Eff.Predef(Predef.TRUE_n,_)}, _)
+ | CallByPosEff({src=lxm;it=Eff.Predef(Predef.FALSE_n,_)}, _)
+ | CallByPosEff({src=lxm;it=Eff.Predef(Predef.ICONST_n _,_)}, _)
+ | CallByPosEff({src=lxm;it=Eff.Predef(Predef.RCONST_n _,_)}, _)
+ (* We do not create an intermediary variable for those,
+ but
+ *)
+ -> if not when_flag then
+ let clk = EvalClock.lookup ve in
+ match snd (List.hd clk) with
+ | On(clock,_) ->
+ let clk_exp = SyntaxTreeCore.NamedClock (Lxm.flagit clock lxm) in
+ CallByPosEff({src=lxm;it=Eff.WHEN clk_exp}, OperEff [ve]), ([],[])
+
+ | (ClockVar _) (* should not occur *)
+ | BaseEff -> ve, ([],[])
+ else
+ ve, ([],[])
| CallByNameEff (by_name_op_eff, fl) ->
let lxm = by_name_op_eff.src in
let fl, eql, vl =
List.fold_left
(fun (fl_acc, eql_acc, vl_acc) (fn, fv) ->
- let fv, (eql, vl) = split_val_exp false node_env fv in
+ let fv, (eql, vl) = split_val_exp false false node_env fv in
((fn,fv)::fl_acc, eql@eql_acc, vl@vl_acc)
)
([],[],[])
@@ -189,31 +215,31 @@ and (split_val_exp : bool -> Eff.local_env -> Eff.val_exp -> Eff.val_exp * split
(* for WITH and HAT, a particular treatment is done because
the val_exp is attached to them *)
| Eff.WITH(ve) ->
- let ve, (eql, vl) = split_val_exp false node_env ve in
+ let ve, (eql, vl) = split_val_exp false false node_env ve in
let by_pos_op_eff = Lxm.flagit (Eff.WITH(ve)) lxm in
let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in
rhs, (eql, vl)
| Eff.HAT(i,ve) ->
- let ve, (eql, vl) = split_val_exp false node_env ve in
+ let ve, (eql, vl) = split_val_exp false false node_env ve in
let by_pos_op_eff = Lxm.flagit (Eff.HAT(i, ve)) lxm in
let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in
rhs, (eql, vl)
- | Eff.WHEN ve -> (* should we create a var for the clock ? *)
- let vel,(eql, vl) = split_val_exp_list false node_env vel in
+ | Eff.WHEN ve -> (* should we create a var for the clock? *)
+ let vel,(eql, vl) = split_val_exp_list true false node_env vel in
let by_pos_op_eff = Lxm.flagit (Eff.WHEN(ve)) lxm in
let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in
rhs, (eql, vl)
| Eff.ARRAY vel ->
- let vel, (eql, vl) = split_val_exp_list false node_env vel in
+ let vel, (eql, vl) = split_val_exp_list false false node_env vel in
let by_pos_op_eff = Lxm.flagit (Eff.ARRAY(vel)) lxm in
let rhs = CallByPosEff(by_pos_op_eff, OperEff []) in
rhs, (eql, vl)
| _ ->
- let vel, (eql, vl) = split_val_exp_list false node_env vel in
+ let vel, (eql, vl) = split_val_exp_list false false node_env vel in
let rhs = CallByPosEff(by_pos_op_eff, OperEff vel) in
rhs, (eql, vl)
in
@@ -259,10 +285,10 @@ and (split_val_exp : bool -> Eff.local_env -> Eff.val_exp -> Eff.val_exp * split
nve, (eql@[eq], vl@nv_l)
-and (split_val_exp_list :
+and (split_val_exp_list : bool ->
bool -> Eff.local_env -> Eff.val_exp list -> Eff.val_exp list * split_acc) =
- fun top_level node_env vel ->
- let vel, accl = List.split (List.map (split_val_exp top_level node_env) vel) in
+ fun when_flag top_level node_env vel ->
+ let vel, accl = List.split (List.map (split_val_exp when_flag top_level node_env) vel) in
let eqll,vll = List.split accl in
let eql, vl = List.flatten eqll, List.flatten vll in
(vel,(eql,vl))
@@ -280,7 +306,7 @@ let (node : Eff.local_env -> Eff.node_exp -> Eff.node_exp) =
let asserts = List.map (fun x -> x.it) b.asserts_eff in
let lxm_asserts = List.map (fun x -> x.src) b.asserts_eff in
let nasserts,(neqs_asserts,nv_asserts) =
- split_val_exp_list true n_env asserts
+ split_val_exp_list false true n_env asserts
in
let nasserts = List.map2 Lxm.flagit nasserts lxm_asserts in
let (neqs, nv) = (neqs@neqs_asserts, nv@nv_asserts) in
diff --git a/src/test/Makefile b/src/test/Makefile
index b878b39a4186bd487e01e81850a60744b880bffa..46a25e8a28610f03707a4aa5754f4f82c13d4a2c 100644
--- a/src/test/Makefile
+++ b/src/test/Makefile
@@ -110,9 +110,12 @@ test_lv4:
for d in ${OK_LUS}; do \
echo -e "\n$(NL)====> $(LC) -lv4 $$d -o /tmp/xx.lus" >> test_lv4.res; \
$(LC0) -lv4 $$d -o /tmp/xx.lus >> test_lv4.res 2>&1 ;\
- set node=$(shell lusinfo /tmp/xx.lus nodes | head -n 1);\
- echo -e "lus2ec /tmp/xx.lus `lusinfo /tmp/xx.lus nodes | head -n 1`" >> test_lv4.res; \
- (lus2ec /tmp/xx.lus `lusinfo /tmp/xx.lus nodes | head -n 1` >> test_lv4.res 2>&1 && echo -n "ok ") || echo " KO!";\
+ for node in `lusinfo /tmp/xx.lus nodes`; do \
+ echo -e "lus2ec /tmp/xx.lus $$node" >> test_lv4.res; \
+ (lus2ec /tmp/xx.lus $$node >> \
+ test_lv4.res 2>&1 && echo -n "ok ") \
+ || echo " KO!";\
+ done; \
done; \
diff -u test_lv4.res.exp test_lv4.res > test_lv4.diff || \
(cat test_lv4.diff ; echo "cf test_lv4.diff"; exit 1)
diff --git a/src/test/should_work/fab_test/morel5.lus b/src/test/should_work/fab_test/morel5.lus
index 3935b14b7363264b6bd33c95632fe19360794bc5..72c473b0b34b11ab091cab70b718fa46a2e167c2 100644
--- a/src/test/should_work/fab_test/morel5.lus
+++ b/src/test/should_work/fab_test/morel5.lus
@@ -6,15 +6,18 @@ type
tube = {in:int; out:int} ;
toto = {titi:tube; tutu:bool} ;
-node morel5(t : toto; b : arrayb; i : arrayi) returns (b1, b2, b3 : bool; i1, i2, i3 : int);
+node morel5(t : toto; b : arrayb; i : arrayi)
+returns (b1, b2, b3 : bool; i1, i2, i3 : int);
let
b1, b2, b3, i1, i2, i3 = tab(t,b,i);
tel
-node tab(yo : toto; tabb : arrayb; tabi : arrayi) returns (b1, b2, b3 : bool; i1, i2, i3 : int);
+node tab(yo : toto; tabb : arrayb; tabi : arrayi)
+returns (b1, b2, b3 : bool; i1, i2, i3 : int);
let
b1, b2, b3 = (tabb[0], tabb[1], tabb[2] or yo.tutu );
- i1, i2, i3 = (tabi[0][0]+tabi[0][1], tabi[1][0]+tabi[1][1] + yo.titi.in , tabi[2][0]+tabi[2][1] + yo.titi.out );
+ i1, i2, i3 = (tabi[0][0]+tabi[0][1], tabi[1][0]+tabi[1][1] +
+ yo.titi.in , tabi[2][0]+tabi[2][1] + yo.titi.out );
--tabb[0] = b;
---tabb[1..2] = [true, false] ;
diff --git a/src/test/test.res.exp b/src/test/test.res.exp
index e4c2210c29f760ce38d98df5bab5fd0e05b0686a..efff42ecd9a67f5a0ac90a5f61cada7164bade60 100644
--- a/src/test/test.res.exp
+++ b/src/test/test.res.exp
@@ -1604,7 +1604,7 @@ var
_v1:_Watch::DISPLAY_POSITION;
_v2:_Watch::DISPLAY_POSITION;
_v3:_Watch::DISPLAY_POSITION;
- _v4:int when time_unit;
+ _v4:int;
_v5:int when time_unit;
_v6:bool when time_unit;
_v7:bool;
@@ -10857,7 +10857,7 @@ var
_v2:int when a;
let
c = _v1 + _v2;
- _v1 = 1 + 1;
+ _v1 = 1 when a + 1 when a;
_v2 = b when a;
tel
-- end of node clock2::clock
diff --git a/src/unifyClock.ml b/src/unifyClock.ml
index 2b202fe5105e6f11ef8f6519827cd3dc026a6700..d3cea2cf14a0ddd5f54e23abff9f7805020ea6ac 100644
--- a/src/unifyClock.ml
+++ b/src/unifyClock.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 28/11/2008 (at 09:54) by Erwan Jahier> *)
+(** Time-stamp: <modified the 09/03/2009 (at 16:11) by Erwan Jahier> *)
open LicDump
@@ -10,55 +10,164 @@ open Eff
let ci2str = LicDump.string_of_clock2
(* exported *)
-(* XXX utiliser une map ! *)
type subst1 = (Ident.t * Ident.t) list
-type subst2 = (int * Eff.clock) list
+
+(**
+ A dedicated kind of substitution tailored to deal with clock variables
+ (Eff.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 Eff.clock type
+ that materialize this fact).
+
+ - When unifying two Eff.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 ",\n\t "
+ (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 -> (string_of_int i)::acc) is [])) ^
+ "}"
+ )::acc
+ )
+ s2.cv_tbl
+ []
+ )) ^ "\n"
+
+let (subst_to_string : subst -> string) =
+ fun (s1,s2) ->
+ let v2s = Ident.to_string in
+ (String.concat ", " (List.map (fun (v1,v2) -> (v2s v1) ^ "/" ^ (v2s v2)) s1)) ^
+ "\nsubst2:\n\t " ^ (subst2_to_string s2)
+
+(******************************************************************************)
+
(* exported *)
-let (empty_subst:subst) = [],[]
+let (empty_subst2:subst2) = { cpt = 0 ; cv_tbl = IntMap.empty }
+let (empty_subst:subst) = [], empty_subst2
let (add_subst1 : Ident.t -> Ident.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 -> Eff.clock -> subst2 -> subst2) =
- fun i c s ->
- if List.mem_assoc i s then s else (i,c)::s
+ 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 : Ident.t -> subst1 -> Ident.t option) =
fun id s ->
try Some (List.assoc id s) with Not_found -> None
let (find_subst2 : int -> subst2 -> Eff.clock option) =
- fun id s ->
- try Some (List.assoc id s) with Not_found -> None
-
+ 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 *)
-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 (new_clock_var : subst -> subst * Eff.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 (get_constant_clock : unit -> Eff.clock) =
- fun () -> ClockVar (get_var_type ())
+let (reset_clock_var : subst -> subst) =
+ fun (s1, s2) -> (s1, empty_subst2)
-(******************************************************************************)
-let (subst_to_string : subst -> string) =
- fun (s1,s2) ->
- let v2s = Ident.to_string 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 -> Eff.clock -> Eff.clock) =
@@ -90,6 +199,7 @@ let rec (apply_subst2:subst -> Eff.clock -> Eff.clock) =
| None -> c
+
let is_clock_var = function
| On(_) | BaseEff -> false | ClockVar _ -> true
@@ -110,7 +220,7 @@ let (f : Lxm.t -> subst -> Eff.clock -> Eff.clock -> subst) =
let s1 = if cv1 = cv2 then s1 else add_subst1 cv2 cv1 s1 in
aux (s1,s2) (clk1, clk2)
| ClockVar i, ClockVar j ->
- if i<>j then s1,(add_subst2 i (ClockVar j) s2) else s1,s2
+ 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
diff --git a/src/unifyClock.mli b/src/unifyClock.mli
index 85985f0cbb60649ca8e415c333855b464ccb8413..ff1aa24db24d3467cc76c2b42bb659982d000dda 100644
--- a/src/unifyClock.mli
+++ b/src/unifyClock.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 28/11/2008 (at 09:16) by Erwan Jahier> *)
+(** Time-stamp: <modified the 09/03/2009 (at 15:20) by Erwan Jahier> *)
(* XXX use Map.t
@@ -22,7 +22,12 @@
XXX Make it abstract?
*)
-type subst = (Ident.t * Ident.t) list * (int * Eff.clock) list
+
+type subst1 = (Ident.t * Ident.t) list
+type subst2
+
+type subst = subst1 * subst2
+(* = (Ident.t * Ident.t) list * (int * Eff.clock) list *)
val empty_subst : subst
@@ -31,15 +36,15 @@ val apply_subst:subst -> Eff.clock -> Eff.clock
(* only apply the part of the subst that deals with clock var *)
val apply_subst2:subst -> Eff.clock -> Eff.clock
+val add_subst2 : int -> Eff.clock -> subst2 -> subst2
+val add_link2 : int -> int -> subst2 -> subst2
-(** Raises an error is the 2 Eff.clock are not unifiable *)
+(** Raises a Compile_error is the 2 Eff.clock are not unifiable *)
val f : Lxm.t -> subst -> Eff.clock -> Eff.clock -> subst
val list : Lxm.t -> Eff.clock list -> subst -> Eff.clock * subst
-(* Stuff to generated fresh var clocks
- XXX bad place, bad name
-*)
-val reset_var_type : unit -> unit
-val get_constant_clock : unit -> Eff.clock
-val get_var_type : unit -> int
+
+val new_clock_var : subst -> subst * Eff.clock
+
+val reset_clock_var : subst -> subst