From a6b571c6f1b199d69e865fca33f998e1d23e1a5e Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Mon, 9 Mar 2009 16:14:12 +0100
Subject: [PATCH] Rewrite the Clock inference of constant. Moreover, when
dumping such constants that are not on the base clock, add the suitable
"when" statement if it was not present in the source code (the lic (and the
ec/lv4) backend does not perform such kind of clock inference for
constants.
---
lv6-ref-man/Makefile | 24 ++--
lv6-ref-man/lv6-ref-man.tex | 4 +-
src/TODO | 3 +
src/evalClock.ml | 165 ++++++++++++++---------
src/evalClock.mli | 5 +-
src/getEff.ml | 9 +-
src/inline.ml | 10 +-
src/licDump.ml | 10 +-
src/predefEvalClock.ml | 49 ++++---
src/predefEvalClock.mli | 7 +-
src/split.ml | 70 +++++++---
src/test/Makefile | 9 +-
src/test/should_work/fab_test/morel5.lus | 9 +-
src/test/test.res.exp | 4 +-
src/unifyClock.ml | 160 ++++++++++++++++++----
src/unifyClock.mli | 23 ++--
16 files changed, 378 insertions(+), 183 deletions(-)
diff --git a/lv6-ref-man/Makefile b/lv6-ref-man/Makefile
index 8073c58f..902b1e6c 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 4425aac6..ec3a277d 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 b22bf8a7..018a9cf7 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 941498b4..870f6685 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 88e1a050..6de00355 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 5c626e9c..ce9a8ef5 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 c3891f45..efedf909 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 f5c5759b..baf9d40f 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 8c3fbd46..6c91c7b8 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 e9406afc..0cf63d80 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 92b0b973..632d60d1 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 b878b39a..46a25e8a 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 3935b14b..72c473b0 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 e4c2210c..efff42ec 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 2b202fe5..d3cea2cf 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 85985f0c..ff1aa24d 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
--
GitLab