From d3061085860ddb4f9534e7b66366c2c984b62f66 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Thu, 14 Aug 2014 16:24:27 +0200
Subject: [PATCH] lic2soc: fix the translation of the current operator into
SOC.
nb : the -exec mode was working because I did not use the generated soc,
which was completely wrong.
Note that to do that, I have modified the CURRENT variant of
Lic.val_exp, to attach it the clock the current holds on. Indeed, the
clock is mandatory to generated correct code...
In an ideal world, this clock information may have explicitely been
set by the user ("current(clk_of_X,X)" instead of "current(X)"), but
for historical reason, it is not the case.
Hence, this information is added as soon as it is available, namely,
during clock checking.
---
_oasis | 7 +++
src/actionsDeps.ml | 3 +-
src/ast2lic.ml | 15 +++--
src/evalClock.ml | 44 ++++++++++++---
src/evalClock.mli | 7 ++-
src/evalType.ml | 10 +++-
src/l2lCheckLoops.ml | 4 +-
src/l2lExpandArrays.ml | 46 +++++++++------
src/l2lExpandNodes.ml | 4 +-
src/l2lSplit.ml | 7 ++-
src/lic.ml | 9 ++-
src/lic2soc.ml | 104 ++++++++++++++++++++++++++++------
src/licDump.ml | 4 +-
src/licEvalClock.ml | 3 +-
src/soc.ml | 7 +--
src/soc2cIdent.ml | 3 +-
src/socExec.ml | 9 +--
src/socExecEvalPredef.ml | 12 +---
src/socExecValue.ml | 10 +++-
src/socPredef.ml | 80 +++++++++++++-------------
src/socPredef2c.ml | 6 +-
src/socUtils.ml | 3 +-
src/unifyType.ml | 8 ++-
test/lus2lic.sum | 34 +++++------
test/lus2lic.time | 2 +-
test/should_work/hanane.lus | 2 +-
todo.org | 109 +++++++++++++++---------------------
27 files changed, 338 insertions(+), 214 deletions(-)
diff --git a/_oasis b/_oasis
index 0ceac8ba..57aec059 100644
--- a/_oasis
+++ b/_oasis
@@ -20,6 +20,13 @@ Executable lus2lic
CompiledObject: native
# CompiledObject: byte
+# to use ocamldebug:
+# - here: set CompiledObject from native to byte
+# - from emacs: [M-x ocamldebug] ./main.byte
+# - from ocamldebug prompt:
+# cd test
+# set arg blabla
+# dir ../src .. ../_build/src /usr/local/soft/ocaml/4.01.0/lib/ocaml/rdbg-plugin/
Library lus4ocaml
diff --git a/src/actionsDeps.ml b/src/actionsDeps.ml
index 81eed47d..6baed0d3 100644
--- a/src/actionsDeps.ml
+++ b/src/actionsDeps.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/07/2014 (at 16:07) by Erwan Jahier> *)
+(** Time-stamp: <modified the 13/08/2014 (at 17:01) by Erwan Jahier> *)
let dbg = (Verbose.get_flag "deps")
@@ -130,6 +130,7 @@ let rec (get_parents : Soc.var_expr -> Soc.var_expr list) =
fun var ->
(* if var = t.[2].field, then it returns (also) t.[2] and t *)
match var with
+ | Soc.Slice(ve,_,_,_,_,_)
| Soc.Field(ve,_,_)
| Soc.Index(ve,_,_) -> ve::(get_parents ve)
| Soc.Var(_,vt)
diff --git a/src/ast2lic.ml b/src/ast2lic.ml
index ef3253f4..09b4f459 100644
--- a/src/ast2lic.ml
+++ b/src/ast2lic.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 05/06/2013 (at 14:41) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/08/2014 (at 16:08) by Erwan Jahier> *)
open Lxm
@@ -30,7 +30,7 @@ let rec (of_type: IdSolver.t -> AstCore.type_exp -> Lic.type_) =
let sz = EvalConst.eval_array_size env szexp in
Array_type_eff (elt_teff, sz)
with EvalConst.EvalArray_error msg ->
- let lxm = lxm_of_val_exp szexp in
+ let lxm = AstCore.lxm_of_val_exp szexp in
raise (Compile_error(lxm, "can't eval type: "^msg))
@@ -166,6 +166,8 @@ let get_abstract_static_params
*)
[]
)
+
+
(* exported *)
let rec of_node
@@ -287,6 +289,7 @@ and check_static_arg
(******************************************************************************)
+
(* exported *)
and (of_eq: IdSolver.t -> AstCore.eq_info srcflagged -> Lic.eq_info srcflagged) =
fun id_solver eq_info ->
@@ -350,7 +353,7 @@ and (translate_val_exp_check : IdSolver.t -> UnifyClock.subst -> AstCore.val_ex
fun id_solver s ve ->
let s,vef = translate_val_exp id_solver s ve in
let lxm = AstCore.lxm_of_val_exp ve in
-(* let vef, tl = EvalType.f id_solver vef in *)
+ (* let vef, tl = EvalType.f id_solver vef in *)
let vef, _, s = EvalClock.f lxm id_solver s vef [] in
s, vef
@@ -434,6 +437,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
in
CallByPosLic(flagit by_pos_op_eff lxm, [array_val_exp])
in
+
let s, vef_core =
match by_pos_op with
| WITH_n(_,_,_) -> assert false (* handled at the top of the function *)
@@ -470,7 +474,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
in
s, const.ve_core
)
- | CURRENT_n -> s, mk_by_pos_op Lic.CURRENT
+ | CURRENT_n -> s, mk_by_pos_op (Lic.CURRENT None)
| PRE_n -> s, mk_by_pos_op Lic.PRE
| ARROW_n -> s, mk_by_pos_op Lic.ARROW
@@ -483,7 +487,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
s,CallByPosLic(flagit Lic.ARROW lxm, [e1;ve_pre])
| _ -> assert false
)
-(* | FBY_n -> s, mk_by_pos_op Lic.FBY *)
+ (* | FBY_n -> s, mk_by_pos_op Lic.FBY *)
| CONCAT_n -> s, mk_by_pos_op Lic.CONCAT
| TUPLE_n -> s, mk_by_pos_op Lic.TUPLE
| ARRAY_n -> s, CallByPosLic(flagit Lic.ARRAY lxm, vel_eff)
@@ -519,7 +523,6 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
in
let vef = { ve_core=vef_core; ve_typ=[]; ve_clk = [] } in
let vef, tl = EvalType.f id_solver vef in
-(* let vef, _, s = EvalClock.f lxm id_solver s vef [] in *)
s,vef
)
diff --git a/src/evalClock.ml b/src/evalClock.ml
index 4bff2f6e..6abb88ef 100644
--- a/src/evalClock.ml
+++ b/src/evalClock.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 25/09/2013 (at 10:58) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/08/2014 (at 16:13) by Erwan Jahier> *)
open AstPredef
@@ -70,7 +70,7 @@ open UnifyClock
- "cil_arg" the list of clocks of arguments (via a rec call to f)
In order to check that this call is correct, we check that both
- terms are unifiable.
+ terms match.
It also modifies the substitution s (acculumated all along the
clock checking of the node) such that:
@@ -84,7 +84,9 @@ let (check_args : Lxm.t -> subst -> Lic.id_clock list -> Lic.id_clock list -> su
assert (List.length cil_par = List.length cil_arg);
let idl_par,cil_par = List.split cil_par
and idl_arg,cil_arg = List.split cil_arg in
- let ns = List.fold_left2 (UnifyClock.f lxm) s cil_arg cil_par in
+ let ns =
+ assert (List.length cil_arg = List.length cil_par);
+ List.fold_left2 (UnifyClock.f lxm) s cil_arg cil_par in
(* should UnifyClock.f modify the *)
(fst s,snd ns)
(* ns *)
@@ -107,7 +109,7 @@ let (check_args : Lxm.t -> subst -> Lic.id_clock list -> Lic.id_clock list -> su
- "left" the list of Lic.left
- "rigth" the list of result clock. (via "get_clock_profile" again)
- and we just need to check that both side are unifiable.
+ and we just need to check that both side match.
*)
let rec (var_info_eff_of_left_eff: Lic.left -> Lic.var_info) =
@@ -143,7 +145,8 @@ let (check_res : Lxm.t -> subst -> Lic.left list -> Lic.id_clock list -> unit) =
let idl_rigth,rigth = List.split rigth
and idl_left, left_ci = List.split left_ci in
let s = (List.combine idl_rigth idl_left)@s1, s2 in
- ignore(List.fold_left2 (UnifyClock.f lxm) s left_ci rigth)
+ assert (List.length left_ci = List.length rigth);
+ ignore(List.fold_left2 (UnifyClock.f lxm) s left_ci rigth)
(******************************************************************************)
@@ -192,12 +195,14 @@ let rec (f : Lxm.t -> IdSolver.t -> subst -> Lic.val_exp -> Lic.clock list ->
(* we split f so that we can reinit the fresh clock var generator *)
let ve, inf_clks, s = f_aux id_solver s ve in
let s =
- if exp_clks = [] then s else
+ if exp_clks = [] then s else (
+ assert (List.length exp_clks = List.length inf_clks);
List.fold_left2
(fun s eclk iclk -> UnifyClock.f lxm s eclk iclk)
s
exp_clks
(List.map (fun (_,clk) -> clk) inf_clks)
+ )
in
let inf_clks = List.map (fun (id,clk) -> id, apply_subst2 s clk) inf_clks in
let clks = snd (List.split inf_clks) in
@@ -215,6 +220,20 @@ and (f_aux : IdSolver.t -> subst -> Lic.val_exp -> Lic.val_exp * Lic.id_clock li
match ve.ve_core with
| CallByPosLic ({it=posop; src=lxm}, args) -> (
let args, cel, s = eval_by_pos_clock id_solver posop lxm args s in
+ let posop,args =
+ (* We attach the clock constructor to CURRENT and the
+ clock var to the list of args. Indeed, the user does not need
+ to specify the clock when it uses current ; hence we add this
+ information as soon as it is computed, i.e., here.
+ *)
+ match posop,args with
+ | CURRENT None, { ve_clk = (On((cc,cv,ct),cv_clk))::_ }::_ ->
+ let cv_val_exp = flagit (Lic.VAR_REF cv) lxm in
+ let cv_val_exp = Lic.CallByPosLic(cv_val_exp,[]) in
+ let cv_val_exp = { ve_core = cv_val_exp ; ve_typ = [ct] ; ve_clk = [cv_clk] } in
+ CURRENT (Some cc), cv_val_exp::args
+ | _ -> posop, args
+ in
let ve = { ve with ve_core = CallByPosLic ({it=posop; src=lxm}, args) } in
List.iter (fun arg -> assert (arg.ve_clk <> [])) args;
ve, cel, s, lxm
@@ -256,7 +275,9 @@ and (f_aux : IdSolver.t -> subst -> Lic.val_exp -> Lic.val_exp * Lic.id_clock li
let new_clk = snd (List.split cel) in
let s, ve =
if ve.ve_clk = [] then (s, { ve with ve_clk = new_clk }) else
- let s = List.fold_left2 (UnifyClock.f lxm) s ve.ve_clk new_clk in
+ let s =
+ assert(List.length ve.ve_clk = List.length new_clk);
+ List.fold_left2 (UnifyClock.f lxm) s ve.ve_clk new_clk in
s, ve
in
let ve = apply_subst_val_exp s ve in
@@ -284,8 +305,12 @@ and (eval_by_pos_clock : IdSolver.t -> Lic.by_pos_op -> Lxm.t -> Lic.val_exp lis
let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in
let args, (cl,s) =
match posop,args with
- | Lic.CURRENT,args -> ( (* we return the clock of the argument *)
- let args, clocks_of_args, s = f_list id_solver s args in
+ (* Depending on the pass (EvalClock is called twice), current
+ can have 1 or 2 args (since we add the clock to
+ Lic.Current during the first pass of clock checking). *)
+ | Lic.CURRENT (Some _), _::arg::[]
+ | Lic.CURRENT None, [arg] -> ( (* we return the clock of the argument *)
+ let args, clocks_of_args, s = f_list id_solver s [arg] in
let current_clock = function
| (id, BaseLic) -> (id, BaseLic)
| (id, On(_,clk)) -> (id, clk)
@@ -355,6 +380,7 @@ and (eval_by_pos_clock : IdSolver.t -> Lic.by_pos_op -> Lxm.t -> Lic.val_exp lis
| _ -> assert false (* "(x1,x2) when node (x,y)" *)
)
)
+ | Lic.HAT(i), [] -> assert false
| Lic.HAT(i), ve::_ ->
let (ve,clk,s) = f_aux id_solver s ve in
[ve],(clk,s)
diff --git a/src/evalClock.mli b/src/evalClock.mli
index 94074c28..ca15507d 100644
--- a/src/evalClock.mli
+++ b/src/evalClock.mli
@@ -1,15 +1,16 @@
-(* Time-stamp: <modified the 12/02/2013 (at 18:06) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/08/2014 (at 12:48) by Erwan Jahier> *)
(** Static evaluation of clocks. *)
open UnifyClock
-(** [f lxm ids s ve cl] checks that [ve] is well-clocked (i.e., for node calls,
+(** [f lxm ids s ve exp_cl] checks that [ve] is well-clocked (i.e., for node calls,
it checks that the argument and the parameter clocks are compatible),
and returns a clock profile that contains all the necessary information
so that the caller can perform additional clock checks.
- nb : if [cl] is empty, no check is done (should be an option type)
+ exp_cl is the expected clock profile; if [cl] is empty, no
+ check is done (should be an option type)
*)
val f : Lxm.t -> IdSolver.t -> subst -> Lic.val_exp -> Lic.clock list ->
Lic.val_exp * Lic.id_clock list * subst
diff --git a/src/evalType.ml b/src/evalType.ml
index f3f3f645..f5f611ba 100644
--- a/src/evalType.ml
+++ b/src/evalType.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 11/04/2013 (at 17:32) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/08/2014 (at 10:42) by Erwan Jahier> *)
open AstPredef
@@ -254,7 +254,13 @@ and eval_by_pos_type
raise(EvalType_error("type mismatch. "))
| _ -> raise_arity_error "" (List.length targs) 2
)
- | Lic.CURRENT
+ | Lic.CURRENT (Some _) -> (
+ let args, targs = List.split (List.map (f id_solver) args) in
+ match targs with
+ | [_;teff] -> None, args, teff
+ | _ -> raise_arity_error "" (List.length targs) 2
+ )
+ | Lic.CURRENT None
| Lic.PRE -> (
let args, targs = List.split (List.map (f id_solver) args) in
match targs with
diff --git a/src/l2lCheckLoops.ml b/src/l2lCheckLoops.ml
index a69ae2fe..2e84fe83 100644
--- a/src/l2lCheckLoops.ml
+++ b/src/l2lCheckLoops.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 11/04/2013 (at 15:30) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/08/2014 (at 16:24) by Erwan Jahier> *)
open Lxm
open Lv6errors
@@ -32,7 +32,7 @@ and
vars_of_by_pos_op s = function
| VAR_REF id -> IdSet.add id s
| PREDEF_CALL(_)
- | ARRAY_SLICE _ | ARRAY_ACCES _ | ARROW | FBY | CURRENT | WHEN _
+ | ARRAY_SLICE _ | ARRAY_ACCES _ | ARROW | FBY | CURRENT _ | WHEN _
| ARRAY | HAT(_) | STRUCT_ACCESS _
| TUPLE | CONCAT | CONST_REF _ | CALL _ | CONST _ -> s
| PRE -> assert false
diff --git a/src/l2lExpandArrays.ml b/src/l2lExpandArrays.ml
index 38df809a..5abf80a3 100644
--- a/src/l2lExpandArrays.ml
+++ b/src/l2lExpandArrays.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/07/2014 (at 17:55) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/08/2014 (at 15:11) by Erwan Jahier> *)
(* Replace structures and arrays by as many variables as necessary.
Since structures can be recursive, it migth be a lot of new variables...
@@ -315,7 +315,7 @@ and (var_trees_of_val_exp :
)
| HAT(_) | CONCAT | ARRAY
| PREDEF_CALL _ | CALL _
- | PRE | ARROW | FBY | CURRENT | WHEN _ | TUPLE -> (
+ | PRE | ARROW | FBY | CURRENT _ | WHEN _ | TUPLE -> (
(* Create a new loc var to alias such expressions *)
let acc, nloc = make_new_loc lctx lxm acc ve in
acc, gen_var_trees (make_val_exp lxm nloc) "" nloc.var_type_eff
@@ -342,9 +342,9 @@ and do_const acc lctx lxm const =
and (break_tuple : Lxm.t -> left list -> val_exp -> Lic.eq_info srcflagged list) =
fun lxm left_list ve ->
- (* Note that this work only if the node expansion has already
- been done! (otherwise, we would not have the same number of
- items in the left and in the rigth part) *)
+ (* Note that this work only if the node expansion has already
+ been done! (otherwise, we would not have the same number of
+ items in the left and in the rigth part) *)
let rec aux ve = (* flatten val exp*)
match ve.ve_core with
| CallByPosLic ({it= TUPLE}, vel)
@@ -360,6 +360,12 @@ and (break_tuple : Lxm.t -> left list -> val_exp -> Lic.eq_info srcflagged list)
List.map
(fun ve1 -> { ve1 with ve_core = CallByPosLic (unop, [ve1])} )
ve1l
+ | CallByPosLic ({ it=CURRENT c ; src=lxm}, [clk;ve]) -> (
+ let vel = aux ve in
+ List.map
+ (fun ve -> { ve with ve_core = CallByPosLic ({it=CURRENT c;src=lxm}, [clk;ve])})
+ vel
+ )
| CallByPosLic (binop, [ve1;ve2]) ->
let ve1l, ve2l = aux ve1, aux ve2 in
if (List.length ve1l <> List.length ve2l) then
@@ -403,20 +409,24 @@ and (break_tuple : Lxm.t -> left list -> val_exp -> Lic.eq_info srcflagged list)
)
| _ -> [ve]
in
- let vel = aux ve in
- if (List.length vel <> List.length left_list) then
+ let lll = List.length left_list in
+ if lll = 1 then (* nothing to break *)
+ [{ src = lxm ; it = (left_list, ve) }]
+ else
+ let vel = aux ve in
+ if (List.length vel <> lll) then
(* migth occur for generic nodes, that needs to be compiled,
but that will not be dumped. *)
- [{ src = lxm ; it = (left_list, ve) }]
- else
- List.map2
- (fun l ve ->
- let clk = [snd (Lic.var_info_of_left l).var_clock_eff] in
- { src = lxm ;
- it = ([l], { ve with ve_typ = [Lic.type_of_left l] ; ve_clk = clk}) }
- )
- left_list
- vel
+ [{ src = lxm ; it = (left_list, ve) }]
+ else
+ List.map2
+ (fun l ve ->
+ let clk = [snd (Lic.var_info_of_left l).var_clock_eff] in
+ { src = lxm ;
+ it = ([l], { ve with ve_typ = [Lic.type_of_left l] ; ve_clk = clk}) }
+ )
+ left_list
+ vel
and (expand_eq :
local_ctx -> acc -> Lic.eq_info srcflagged -> acc) =
@@ -457,7 +467,7 @@ and (expand_val_exp: local_ctx -> acc -> val_exp -> val_exp * acc) =
in
TUPLE, acc, unfold i
| ARRAY | CONCAT | PREDEF_CALL _ | CALL _
- | PRE | ARROW | FBY | CURRENT | WHEN _ | TUPLE | CONST _
+ | PRE | ARROW | FBY | CURRENT _ | WHEN _ | TUPLE | CONST _
->
let vel,acc = expand_val_exp_list lctx acc vel in
by_pos_op, acc, vel
diff --git a/src/l2lExpandNodes.ml b/src/l2lExpandNodes.ml
index 73dcd224..7fe9a2cd 100644
--- a/src/l2lExpandNodes.ml
+++ b/src/l2lExpandNodes.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 24/09/2013 (at 10:56) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/08/2014 (at 16:25) by Erwan Jahier> *)
open Lxm
@@ -96,7 +96,7 @@ and (subst_in_val_exp : subst -> val_exp -> val_exp) =
VAR_REF id'
| WHEN(clk) -> WHEN(subst_in_clock s clk)
| HAT(i) -> HAT(i)
- | PREDEF_CALL _| CALL _ | PRE | ARROW | FBY | CURRENT | TUPLE
+ | PREDEF_CALL _| CALL _ | PRE | ARROW | FBY | CURRENT _ | TUPLE
| ARRAY | CONCAT | STRUCT_ACCESS _ | ARRAY_ACCES _ | ARRAY_SLICE _
| CONST _
-> by_pos_op
diff --git a/src/l2lSplit.ml b/src/l2lSplit.ml
index 3525ec57..6b2b5acd 100644
--- a/src/l2lSplit.ml
+++ b/src/l2lSplit.ml
@@ -58,7 +58,7 @@ let to_be_broken = function
| CallByPosLic({ it = Lic.ARROW }, _) -> true
| CallByPosLic({ it = Lic.FBY }, _) -> true
| CallByPosLic({ it = Lic.PRE }, _) -> true
- | CallByPosLic({ it = Lic.CURRENT }, _) -> true
+ | CallByPosLic({ it = Lic.CURRENT _ }, _) -> true
| CallByPosLic({ it = Lic.TUPLE }, _) -> true
| CallByPosLic({ it = Lic.WHEN _ }, _) -> true
| CallByPosLic({ it = Lic.PREDEF_CALL({ it = (("Lustre","if"),[]) })}, _) -> true
@@ -99,6 +99,11 @@ let (break_it_do : val_exp -> val_exp list) =
let vel = get_vel_from_tuple ve in
List.map
(fun ve -> { ve with ve_core=CallByPosLic({it=op;src=lxm}, [ve])})
+ vel
+ | CallByPosLic({it=CURRENT c ; src=lxm }, [clk;ve]) ->
+ let vel = get_vel_from_tuple ve in
+ List.map
+ (fun ve -> { ve with ve_core=CallByPosLic({it=CURRENT c;src=lxm}, [clk;ve])})
vel
| CallByPosLic({it=op ; src=lxm }, [ve1;ve2]) ->
let vel1 = get_vel_from_tuple ve1
diff --git a/src/lic.ml b/src/lic.ml
index 3142759a..5b186657 100644
--- a/src/lic.ml
+++ b/src/lic.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 04/06/2013 (at 14:59) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/08/2014 (at 09:48) by Erwan Jahier> *)
(** Define the Data Structure representing Compiled programs. *)
@@ -177,7 +177,7 @@ and by_pos_op =
| PRE
| ARROW
| FBY
- | CURRENT
+ | CURRENT of Ident.long option (* we know the clock after clock checking *)
| WHEN of clock
| TUPLE
@@ -527,6 +527,11 @@ let (is_extern_const : const -> bool) =
let type_of_val_exp ve = ve.ve_typ
+let rec lxm_of_val_exp ve =
+ match ve.ve_core with
+ | CallByPosLic (x,_) -> x.src
+ | CallByNameLic (x, _) -> x.src
+ | Merge(ve, _) -> lxm_of_val_exp ve
(* Ne doit être appelée que pour les constantes simple *)
let (type_of_const: const -> type_) =
diff --git a/src/lic2soc.ml b/src/lic2soc.ml
index 3372af58..111b9804 100644
--- a/src/lic2soc.ml
+++ b/src/lic2soc.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 10/07/2014 (at 10:07) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/08/2014 (at 10:34) by Erwan Jahier> *)
(* XXX ce module est mal écrit. A reprendre. (R1) *)
@@ -200,7 +200,7 @@ let rec get_leaf: (LicPrg.t -> Lic.val_exp -> Soc.var_expr list option) =
| Lic.HAT _
| Lic.ARROW
| Lic.FBY
- | Lic.CURRENT
+ | Lic.CURRENT _
| Lic.WHEN(_)
| Lic.CONCAT
-> None
@@ -386,7 +386,7 @@ let rec (val_exp_to_filter: LicPrg.t -> Lic.val_exp -> Soc.var_expr) =
| PRE
| ARROW
| FBY
- | CURRENT
+ | CURRENT _
| CONCAT
| HAT _
| ARRAY
@@ -475,7 +475,7 @@ let (node_key_of_pos_op : Lic.by_pos_op -> Lic.node_key) = fun op ->
| PRE -> ("","Lustre::pre"),[]
| ARROW -> ("","Lustre::arrow" ),[]
| FBY-> ("","Lustre::fby"),[]
- | CURRENT -> ("","Lustre::current"),[]
+ | CURRENT _ -> ("","Lustre::current"),[]
| CONCAT-> ("","Lustre::concat"),[]
| ARRAY -> ("","Lustre::array"),[]
| ARRAY_SLICE _ -> ("","Lustre::array_slice"),[]
@@ -484,7 +484,6 @@ let (node_key_of_pos_op : Lic.by_pos_op -> Lic.node_key) = fun op ->
| _ -> assert false
-
let (get_exp_type : Soc.var_expr list -> Data.t list) =
fun vl ->
let tl = List.map Soc.data_type_of_var_expr vl in
@@ -536,15 +535,14 @@ let rec (actions_of_expression_acc: Lxm.t -> Soc.tbl ->
| Lic.ARRAY_ACCES _ | Lic.STRUCT_ACCESS _ | Lic.TUPLE
-> assert false (* should not occur: handled via get_leaf *)
| Lic.WHEN ck -> (
- (* L'opérateur when n'est pas un composant, il modifie simplement
- les conditions de traitement des expressions. *)
+ (* 'when' does not generate any soc, but it states
+ when expressions are executed . *)
let ctx, actions, inputs, mems, deps =
actions_of_expression_list by_pos_op_flg.src soc_tbl clk lpl acc val_exp_list
in
let ctx, outputs, actions_reclocked =
match actions with
- | [] -> (* L'expression du when est une feuille, on créé quand même
- une nouvelle action pour clocker la feuille. *)
+ | [] -> (* val_exp is a leaf x. *)
ctx, lpl, [ck, inputs, lpl, Soc.Assign, lxm]
| _ -> ctx, inputs,
(* Remplacement de l'horloge des actions de l'expression par
@@ -553,11 +551,82 @@ let rec (actions_of_expression_acc: Lxm.t -> Soc.tbl ->
in
ctx, actions_reclocked, outputs, mems, deps
)
+(* | CURRENT -> (
+ let ctx, actions, inputs, mems, deps =
+ actions_of_expression_list by_pos_op_flg.src soc_tbl clk lpl acc val_exp_list
+ in
+ let ck = match expr.Lic.ve_clk with
+ | [On((_cc,_cv,_ct),ck)] -> ck
+ | [BaseLic] -> BaseLic
+ | _ -> assert false (* SNO! *)
+ in
+ let ctx, outputs, actions_reclocked =
+ match actions with
+ | [] -> ctx, lpl, [ck, inputs, lpl, Soc.Assign, lxm]
+ | _ ->
+ ctx, inputs, List.map (fun (_, i,o,op,lxm) -> ck,i,o,op,lxm) actions
+ in
+*)
+ (* XXX il faudrait que j'arrive à dire que les variables
+ contenues dans "inputs" sont rémanentes -> un champ supplémentaire
+ à e2a_acc ?
+
+ Admettons. Je fais quoi ensuite de cette liste de variables ?
+ Pour commencer je positionne le champ memory à autre chose que No_mem
+ si nécessaire.
+
+ Ensuite il faudrait que dans Soc.step_impl.Goal, j'ai 2 ensembles
+ de variables locales : les remanentes et les autres.
+
+ Autre solution : Quand un soc a de la mémoire, toutes ses variables
+ locales doivent etre rémanentes (aka static). boarf.
+
+ -----------------------------------------------------
+ en effet, quand on écrit l'expression "current(y)",
+ si on arrive à garantir que y est rémanent, il n'y a juste rien à
+ faire. Que l'horloge de y soit activée ou pas.
+
+ écrire current dans un programme, ca veut dire "souviens toi de la
+ valeur que je prend".
+
+ Bon, bien sur, on pourrait passer par un soc
+ explicite ayant une memoire qui est mise à jour à
+ chaque step, et utilisé ou pas selon la valeur de l'horloge.
+
+ C'est moins ad-hoc, mais moins efficace.
+ ----------------------------------------------------
+ Non, ce qu'il faut faire, c'est faire en sorte que cette variable
+ soit une memoire du soc ou elle est utilisée, au meme titre
+ que les instances de noeud à mémoire. Pour l'instant ca n'est pas
+ prevu dans Soc.t, mais il faut le rajouter.
+
+ En modifiant le type instance ? Pour l'instant c'est
+
+ type instance = ident * key
+
+ il faudrait mettre
+
+ type mem_cell = Instance of ident * key
+ | Cell of var
+
+ et le champ memory ne sert pas à grand chose on dirait. A part pour
+ les noeuds externes pour indiquer qu'ils ont de la mémoire.
+
+ Admettons qu'on le garde ; l'info de type associé au variant Mem
+ n'a vraiment rien a faire la. Mais dans ce cas, un booleen
+ have_mem suffit.
+
+
+ ctx, actions_reclocked, outputs, mems, deps
+ )
+ *)
+
+ | CURRENT _
| Lic.ARRAY_SLICE _
- | CURRENT (* todo ? *)
| CALL _ | PREDEF_CALL _
| HAT _ | ARRAY | PRE | ARROW | FBY | CONCAT -> (
(* retreive the soc of "expr" in soc_tbl *)
+
let soc : Soc.t =
let args_types : Data.t list =
List.map lic_to_data_type
@@ -574,13 +643,14 @@ let rec (actions_of_expression_acc: Lxm.t -> Soc.tbl ->
let (sk_name, sk_prof,_) = sk in
let sk,fby_init_opt =
let init = val_exp_to_filter ctx.prg (List.hd val_exp_list) in
- if by_pos_op_flg.it = Lic.FBY then
- (sk_name, sk_prof, Soc.MemInit init), Some init
- else if by_pos_op_flg.it = Lic.ARROW then
- let init = Soc.Const("_true", Data.Bool) in
- (sk_name, sk_prof, Soc.MemInit init), Some init
- else
- sk, None
+ match by_pos_op_flg.it with
+ | Lic.FBY -> (sk_name, sk_prof, Soc.MemInit init), Some init
+ | Lic.ARROW ->
+ let init = Soc.Const("_true", Data.Bool) in
+ (sk_name, sk_prof, Soc.MemInit init), Some init
+ | Lic.CURRENT (Some cc) ->
+ (sk_name, sk_prof, Soc.Curr(cc)), None
+ | _ -> sk, None
in
try Soc.SocMap.find sk soc_tbl
with Not_found ->
diff --git a/src/licDump.ml b/src/licDump.ml
index f36b610f..5926d00c 100644
--- a/src/licDump.ml
+++ b/src/licDump.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 03/07/2014 (at 14:03) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/08/2014 (at 10:59) by Erwan Jahier> *)
open Lv6errors
open Printf
@@ -419,7 +419,7 @@ and (string_of_by_pos_op_eff: Lic.by_pos_op srcflagged -> Lic.val_exp list -> st
(if is_a_tuple ve1 then tuple_par [ve2] else string_of_val_exp_eff ve2)
| WHEN clk, vel -> (tuple vel) ^ (string_of_clock clk)
- | CURRENT,_ -> "current " ^ tuple_par vel
+ | CURRENT _,_ -> "current " ^ tuple_par (if global_opt.ec then List.tl vel else vel)
| TUPLE,_ -> (tuple vel)
| CONCAT, [ve1; ve2] ->
(string_of_val_exp_eff ve1) ^ " | " ^ (string_of_val_exp_eff ve2)
diff --git a/src/licEvalClock.ml b/src/licEvalClock.ml
index b2d0d944..a625d6f9 100644
--- a/src/licEvalClock.ml
+++ b/src/licEvalClock.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 12/02/2013 (at 17:51) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/08/2014 (at 16:59) by Erwan Jahier> *)
open AstPredef
@@ -47,6 +47,7 @@ let f
| 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
+ | ILT_n|ILTE_n|IGT_n|IGTE_n|RLT_n|RLTE_n|RGT_n|RGTE_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
diff --git a/src/soc.ml b/src/soc.ml
index cd5bd889..cbe85d10 100644
--- a/src/soc.ml
+++ b/src/soc.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 01/07/2014 (at 15:40) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/08/2014 (at 10:01) by Erwan Jahier> *)
(** Synchronous Object Component *)
@@ -22,6 +22,7 @@ type key_opt =
| Nomore
| Slic of int * int * int (* for slices *)
| MemInit of var_expr (* for fby *)
+ | Curr of Ident.long (* clock constructor for current *)
type key =
ident *
@@ -85,14 +86,12 @@ type memory =
| Mem_hidden (* for extern nodes *)
type t = {
- (* les memoires de l'objet sont calculées par l'interpreteur (ou l'objet C) *)
key : key;
profile : var list * var list;
- instances : instance list;
-(* init : step_method option; *)
step : step_method list; (* the order in the list is a valid w.r.t.
the partial order defined in precedences *)
precedences : precedence list; (* partial order over step methods *)
+ instances : instance list;
memory : memory;
(* Do this soc have a memory (pre, fby) + its type *)
}
diff --git a/src/soc2cIdent.ml b/src/soc2cIdent.ml
index a2d642ae..292d6d69 100644
--- a/src/soc2cIdent.ml
+++ b/src/soc2cIdent.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 10/07/2014 (at 11:54) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/08/2014 (at 10:32) by Erwan Jahier> *)
let colcol = Str.regexp "::"
let id2s id = (* XXX Refuser les noms de module à la con plutot *)
@@ -43,6 +43,7 @@ let rec (type_to_short_string : Data.t -> string) =
let (key_op2str : Soc.key_opt -> string) = function
| Nomore -> ""
+ | Curr(cc) -> Ident.string_of_long2 cc
| Slic(b,e,s) -> Printf.sprintf "_slice_%d_%d_%d" b e s
| MemInit(var_expr) -> "_" ^
(* XXX This is wrong because hash is not an injection !!! *)
diff --git a/src/socExec.ml b/src/socExec.ml
index 6beda2ba..14fbba2e 100644
--- a/src/socExec.ml
+++ b/src/socExec.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 07/08/2014 (at 15:17) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/08/2014 (at 09:36) by Erwan Jahier> *)
open Soc
open Data
@@ -83,7 +83,8 @@ let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx
if v = U || v = B true then
(* We are on the first step of node_soc;
- we assign the output var to the default values *)
- List.fold_left2 assign_expr ctx dft_cst vel_out
+ (assert (List.length dft_cst = List.length vel_out);
+ List.fold_left2 assign_expr ctx dft_cst vel_out)
else
(* We are not on the first step of node_soc; hence we do nothing
and the output will keep their previous value. *)
@@ -139,8 +140,8 @@ and (do_gao : Lxm.t -> Soc.tbl -> SocExecValue.ctx -> gao -> SocExecValue.ctx)
)
| Call(vel_out, Assign, vel_in) -> (
let ctx =
- try List.fold_left2 assign_expr ctx vel_in vel_out
- with _ -> assert false
+ assert (List.length vel_in = List.length vel_out);
+ List.fold_left2 assign_expr ctx vel_in vel_out
in
ctx
)
diff --git a/src/socExecEvalPredef.ml b/src/socExecEvalPredef.ml
index aa012dd6..038fb859 100644
--- a/src/socExecEvalPredef.ml
+++ b/src/socExecEvalPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/06/2014 (at 15:02) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/08/2014 (at 15:39) by Erwan Jahier> *)
open SocExecValue
open Data
@@ -307,14 +307,6 @@ let lustre_concat ctx =
in
{ ctx with s = sadd ctx.s vn vv }
-let lustre_current ctx =
- let (vn,vv) =
- match ([get_val "x" ctx]) with
- | [v] -> "z"::ctx.cpath, v
- | _ -> assert false
- in
- { ctx with s = sadd ctx.s vn vv }
-
let lustre_arrow ctx =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx;
@@ -386,7 +378,7 @@ let (get: Soc.key -> (ctx -> ctx)) =
| "Lustre::concat" -> lustre_concat
| "Lustre::arrow" -> lustre_arrow
- | "Lustre::current" -> lustre_current
+ | "Lustre::current" -> assert false
| "Lustre::merge" -> lustre_merge tl
| "Lustre::array_slice" -> lustre_slice tl si_opt
diff --git a/src/socExecValue.ml b/src/socExecValue.ml
index bb473ca2..9582b3aa 100644
--- a/src/socExecValue.ml
+++ b/src/socExecValue.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 01/07/2014 (at 14:42) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/08/2014 (at 09:32) by Erwan Jahier> *)
let dbg = (Verbose.get_flag "exec")
@@ -322,7 +322,9 @@ let (substitute_args_and_params : var_expr list -> var list -> ctx -> substs) =
fun args params ctx ->
assert (List.length args = List.length params);
let arg_ctx = { ctx with cpath = List.tl ctx.cpath } in
- let s = List.fold_left2
+ let s =
+ assert (List.length args = List.length params);
+ List.fold_left2
(fun acc arg (pn,_) -> sadd acc (pn::ctx.cpath) (get_value arg_ctx arg))
ctx.s args params
in
@@ -331,7 +333,9 @@ let (substitute_args_and_params : var_expr list -> var list -> ctx -> substs) =
let (substitute_params_and_args : var list -> var_expr list -> ctx -> substs) =
fun params args ctx ->
assert (List.length args = List.length params);
- let s = List.fold_left2
+ let s =
+ assert (List.length args = List.length params);
+ List.fold_left2
(fun acc arg (pn,_) ->
let path = List.tl ctx.cpath in
let v = get_val pn ctx in
diff --git a/src/socPredef.ml b/src/socPredef.ml
index c986afb9..97e13314 100644
--- a/src/socPredef.ml
+++ b/src/socPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 07/08/2014 (at 14:09) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/08/2014 (at 16:14) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
@@ -165,35 +165,36 @@ let of_soc_key : Soc.key -> Soc.t =
(* Those have instances *)
| "Lustre::current" -> (
- let _,tl,_ = sk in
- let t = List.hd tl in
- let pre_mem:var = (get_mem_name sk t, t) in
- let prof = sp tl in
- let v1,vout = match prof with ([v1],[vout]) -> v1,vout | _ -> assert false in
- {
- key = sk;
- profile = (sp tl);
- instances = [];
- memory = Mem (t); (* so that pre_mem exist *)
- step = [
- {
- name = "get";
- lxm = Lxm.dummy "predef soc";
- idx_ins = [];
- idx_outs = [0];
- impl = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]);
- };
- {
- name = "set";
- lxm = Lxm.dummy "predef soc";
- idx_ins = [0];
- idx_outs = [];
- impl = Gaol([pre_mem],[Call([Var(pre_mem)], Assign, [Var(v1)])]);
- };
- ];
- precedences = ["get", ["set"]];
- }
- )
+ let tl,cc = match sk with
+ | _,tl, Curr(cc) -> tl,cc
+ | _,_,_ -> assert false
+ in
+ let t = List.hd (List.tl tl) in
+ let mem:var = (get_mem_name sk t, t) in
+ let prof:var list * var list = sp tl in
+ let cv,vin,vout = match prof with ([cv;vin],[vout]) -> cv,vin,vout | _ -> assert false in
+ {
+ key = sk;
+ profile = (sp tl);
+ instances = [];
+ memory = Mem (t);
+ step = [
+ {
+ name = "step";
+ lxm = Lxm.dummy "predef soc";
+ idx_ins = [0;1];
+ idx_outs = [0];
+ impl =
+ Gaol([],
+ [Case((fst cv),[
+ (Ident.string_of_long2 cc, [Call([Var(mem)], Assign, [Var(vin)])])]);
+ Call([Var(vout)], Assign, [Var(mem)])])
+ };
+ ];
+ precedences = [];
+ }
+ )
+
| "Lustre::pre" ->
let _,tl,_ = sk in
let t = List.hd tl in
@@ -211,18 +212,18 @@ let of_soc_key : Soc.key -> Soc.t =
lxm = Lxm.dummy "predef soc";
idx_ins = [];
idx_outs = [0];
-(* impl = Predef; *)
- impl = Gaol([],[Call([Var(vout)], Assign, [Var(pre_mem)])]);
-(* impl = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]); *)
+ (* impl = Predef; *)
+ impl = Gaol([],[Call([Var(vout)], Assign, [Var(pre_mem)])]);
+ (* impl = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]); *)
};
{
name = "set";
lxm = Lxm.dummy "predef soc";
idx_ins = [0];
idx_outs = [];
-(* impl = Predef; *)
- impl = Gaol([],[Call([Var(pre_mem)], Assign, [Var(v1)])]);
-(* impl = Gaol([pre_mem],[Call([Var(pre_mem)], Assign, [Var(v1)])]); *)
+ (* impl = Predef; *)
+ impl = Gaol([],[Call([Var(pre_mem)], Assign, [Var(v1)])]);
+ (* impl = Gaol([pre_mem],[Call([Var(pre_mem)], Assign, [Var(v1)])]); *)
};
];
precedences = ["set", ["get"]];
@@ -523,10 +524,11 @@ let (soc_interface_of_pos_op:
let concrete_type = List.nth types 0 in
let soc = of_soc_key (("Lustre::pre"), types@[concrete_type], Nomore) in
instanciate_soc soc concrete_type
- | Lic.CURRENT, _, _ ->
- let concrete_type = List.nth types 0 in
- let soc = of_soc_key (("Lustre::current"), types@[concrete_type], Nomore) in
+ | Lic.CURRENT (Some(cc)), _, _ ->
+ let concrete_type = List.nth types 1 in
+ let soc = of_soc_key (("Lustre::current"), types@[concrete_type], Curr(cc)) in
instanciate_soc soc concrete_type
+ | Lic.CURRENT (_), _, _ -> assert false
| Lic.ARROW, _, _ ->
let concrete_type = List.nth types 0 in
let soc = of_soc_key (("Lustre::arrow"), types@[concrete_type],
diff --git a/src/socPredef2c.ml b/src/socPredef2c.ml
index 39e01a62..68148f2e 100644
--- a/src/socPredef2c.ml
+++ b/src/socPredef2c.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 01/07/2014 (at 14:23) by Erwan Jahier> *)
+(* Time-stamp: <modified the 14/08/2014 (at 16:16) by Erwan Jahier> *)
open Data
open Soc
@@ -35,6 +35,7 @@ let (lustre_impl : Soc.key -> string) =
(* use gen_assign? *)
Printf.sprintf" %s.z = (!%s.x || %s.y);\n" ctx ctx ctx
+
let (lustre_arrow : Soc.key -> string) =
fun sk ->
let x,y,z = "ctx->x", "ctx->y", "ctx->z" in
@@ -198,6 +199,7 @@ let (get_key: Soc.key -> string) =
| "Lustre::rif"
| "Lustre::iif" -> lustre_ite sk
+ | "Lustre::current" -> assert false
| "Lustre::arrow" -> lustre_arrow sk
| "Lustre::merge" -> lustre_merge sk
@@ -206,7 +208,7 @@ let (get_key: Soc.key -> string) =
| "Lustre::concat" -> lustre_concat sk
| "Lustre::array_slice" -> lustre_slice sk
- | "Lustre::current" -> assert false (* o*)
+
| "Lustre::nor" -> assert false (* ougth to be translated into boolred *)
| "Lustre::diese" -> assert false (* ditto *)
diff --git a/src/socUtils.ml b/src/socUtils.ml
index 8e7b6fdc..44c09bce 100644
--- a/src/socUtils.ml
+++ b/src/socUtils.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 01/07/2014 (at 14:45) by Erwan Jahier> *)
+(** Time-stamp: <modified the 14/08/2014 (at 11:11) by Erwan Jahier> *)
open Soc
@@ -81,6 +81,7 @@ let string_of_soc_key_ff: (Soc.key -> Format.formatter -> unit) =
(String.concat " -> " (List.map string_of_type_ref types)));
(match si_opt with
| Nomore -> ()
+ | Curr(cc) -> fprintf ff "%s" (Ident.string_of_long2 cc)
| Slic(f,l,step) -> fprintf ff "[%d .. %d step %d]" f l step
| MemInit ve -> string_of_filter_ff ve ff
)
diff --git a/src/unifyType.ml b/src/unifyType.ml
index ac0a96c6..8fd3a1cb 100644
--- a/src/unifyType.ml
+++ b/src/unifyType.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 26/06/2014 (at 11:16) by Erwan Jahier> *)
+(* Time-stamp: <modified the 13/08/2014 (at 09:40) by Erwan Jahier> *)
(*
12/07. Premier pas vers une méthode un peu plus standard :
@@ -70,7 +70,7 @@ let f (l1: Lic.type_ list) (l2: Lic.type_ list): t =
(** USELESS ??? *)
let fl1 = List.map (fun (_,(te,_)) -> te) fl1
and fl2 = List.map (fun (_,(te,_)) -> te) fl2 in
- assert(List.length fl1 = List.length fl1);
+ assert(List.length fl1 = List.length fl2);
List.fold_left2 unify_do_acc Equal fl1 fl2
| TypeVar AnyNum, TypeVar Any
| TypeVar Any, TypeVar AnyNum -> Unif (TypeVar AnyNum)
@@ -110,7 +110,9 @@ let f (l1: Lic.type_ list) (l2: Lic.type_ list): t =
if (List.length l1 <> List.length l2) then
Ko("\n** "^ l1_str ^ " and " ^ l2_str ^ " are not unifiable (bad arity)")
else
- let res = List.fold_left2 unify_do_acc Equal l1 l2 in
+ let res =
+ assert (List.length l1 = List.length l2);
+ List.fold_left2 unify_do_acc Equal l1 l2 in
Verbose.printf ~flag:dbg
"#DBG: UnifyType.f (%s) with (%s) gives %s\n"
(Lic.string_of_type_list l1)
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index 5dd9cd6d..85424e82 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Thu Aug 7 16:41:50 2014
+Test Run By jahier on Thu Aug 14 16:18:48 2014
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
@@ -29,7 +29,7 @@ PASS: ./myec2c {-o ./tmp/ck5.c ./tmp/ck5.ec}
PASS: ../utils/test_lus2lic_no_node should_work/ck5.lus
PASS: ./lus2lic {-2c should_work/ck5.lus -n ck5}
PASS: gcc ck5_ck5.c ck5_ck5_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/ck5.lus
+PASS: ../utils/compare_exec_and_2c should_work/ck5.lus
PASS: ./lus2lic {-o ./tmp/normal.lic should_work/normal.lus}
PASS: ./lus2lic {-ec -o ./tmp/normal.ec should_work/normal.lus}
PASS: ./myec2c {-o ./tmp/normal.c ./tmp/normal.ec}
@@ -630,7 +630,7 @@ PASS: ./myec2c {-o ./tmp/clock_ite.c ./tmp/clock_ite.ec}
PASS: ../utils/test_lus2lic_no_node should_work/clock_ite.lus
PASS: ./lus2lic {-2c should_work/clock_ite.lus -n clock_ite}
PASS: gcc clock_ite_clock_ite.c clock_ite_clock_ite_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/clock_ite.lus
+PASS: ../utils/compare_exec_and_2c should_work/clock_ite.lus
PASS: ./lus2lic {-o ./tmp/morel4.lic should_work/morel4.lus}
PASS: ./lus2lic {-ec -o ./tmp/morel4.ec should_work/morel4.lus}
PASS: ./myec2c {-o ./tmp/morel4.c ./tmp/morel4.ec}
@@ -881,7 +881,7 @@ PASS: ./myec2c {-o ./tmp/CURRENT.c ./tmp/CURRENT.ec}
PASS: ../utils/test_lus2lic_no_node should_work/CURRENT.lus
PASS: ./lus2lic {-2c should_work/CURRENT.lus -n CURRENT}
PASS: gcc CURRENT_CURRENT.c CURRENT_CURRENT_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/CURRENT.lus
+PASS: ../utils/compare_exec_and_2c should_work/CURRENT.lus
PASS: ./lus2lic {-o ./tmp/left.lic should_work/left.lus}
PASS: ./lus2lic {-ec -o ./tmp/left.ec should_work/left.lus}
PASS: ./myec2c {-o ./tmp/left.c ./tmp/left.ec}
@@ -904,7 +904,7 @@ PASS: ./myec2c {-o ./tmp/multiclock.c ./tmp/multiclock.ec}
PASS: ../utils/test_lus2lic_no_node should_work/multiclock.lus
PASS: ./lus2lic {-2c should_work/multiclock.lus -n multiclock}
PASS: gcc multiclock_multiclock.c multiclock_multiclock_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/multiclock.lus
+PASS: ../utils/compare_exec_and_2c should_work/multiclock.lus
PASS: ./lus2lic {-o ./tmp/nc2.lic should_work/nc2.lus}
PASS: ./lus2lic {-ec -o ./tmp/nc2.ec should_work/nc2.lus}
PASS: ./myec2c {-o ./tmp/nc2.c ./tmp/nc2.ec}
@@ -963,7 +963,7 @@ PASS: ./myec2c {-o ./tmp/TIME_STABLE.c ./tmp/TIME_STABLE.ec}
PASS: ../utils/test_lus2lic_no_node should_work/TIME_STABLE.lus
PASS: ./lus2lic {-2c should_work/TIME_STABLE.lus -n TIME_STABLE}
PASS: gcc TIME_STABLE_TIME_STABLE.c TIME_STABLE_TIME_STABLE_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/TIME_STABLE.lus
+PASS: ../utils/compare_exec_and_2c should_work/TIME_STABLE.lus
PASS: ./lus2lic {-o ./tmp/cpt.lic should_work/cpt.lus}
PASS: ./lus2lic {-ec -o ./tmp/cpt.ec should_work/cpt.lus}
PASS: ./myec2c {-o ./tmp/cpt.c ./tmp/cpt.ec}
@@ -1047,7 +1047,7 @@ PASS: ./myec2c {-o ./tmp/bob.c ./tmp/bob.ec}
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/bob.lus
PASS: ./lus2lic {-2c should_work/bob.lus -n bob}
PASS: gcc bob_bob.c bob_bob_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/bob.lus
+PASS: ../utils/compare_exec_and_2c should_work/bob.lus
PASS: ./lus2lic {-o ./tmp/notTwo.lic should_work/notTwo.lus}
PASS: ./lus2lic {-ec -o ./tmp/notTwo.ec should_work/notTwo.lus}
PASS: ./myec2c {-o ./tmp/notTwo.c ./tmp/notTwo.ec}
@@ -1160,7 +1160,7 @@ PASS: ./myec2c {-o ./tmp/ck4.c ./tmp/ck4.ec}
PASS: ../utils/test_lus2lic_no_node should_work/ck4.lus
PASS: ./lus2lic {-2c should_work/ck4.lus -n ck4}
PASS: gcc ck4_ck4.c ck4_ck4_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/ck4.lus
+PASS: ../utils/compare_exec_and_2c should_work/ck4.lus
PASS: ./lus2lic {-o ./tmp/map_red_iter.lic should_work/map_red_iter.lus}
PASS: ./lus2lic {-ec -o ./tmp/map_red_iter.ec should_work/map_red_iter.lus}
PASS: ./myec2c {-o ./tmp/map_red_iter.c ./tmp/map_red_iter.ec}
@@ -1184,7 +1184,7 @@ PASS: ./myec2c {-o ./tmp/filliter.c ./tmp/filliter.ec}
PASS: ../utils/test_lus2lic_no_node should_work/filliter.lus
PASS: ./lus2lic {-2c should_work/filliter.lus -n filliter}
PASS: gcc filliter_filliter.c filliter_filliter_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/filliter.lus
+PASS: ../utils/compare_exec_and_2c should_work/filliter.lus
PASS: ./lus2lic {-o ./tmp/minmax4.lic should_work/minmax4.lus}
PASS: ./lus2lic {-ec -o ./tmp/minmax4.ec should_work/minmax4.lus}
PASS: ./myec2c {-o ./tmp/minmax4.c ./tmp/minmax4.ec}
@@ -1315,7 +1315,7 @@ PASS: ./myec2c {-o ./tmp/X2.c ./tmp/X2.ec}
PASS: ../utils/test_lus2lic_no_node should_work/X2.lus
PASS: ./lus2lic {-2c should_work/X2.lus -n X2}
PASS: gcc X2_X2.c X2_X2_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/X2.lus
+PASS: ../utils/compare_exec_and_2c should_work/X2.lus
PASS: ./lus2lic {-o ./tmp/alias.lic should_work/alias.lus}
PASS: ./lus2lic {-ec -o ./tmp/alias.ec should_work/alias.lus}
PASS: ./myec2c {-o ./tmp/alias.c ./tmp/alias.ec}
@@ -1326,10 +1326,10 @@ PASS: ../utils/compare_exec_and_2c should_work/alias.lus
PASS: ./lus2lic {-o ./tmp/hanane.lic should_work/hanane.lus}
PASS: ./lus2lic {-ec -o ./tmp/hanane.ec should_work/hanane.lus}
PASS: ./myec2c {-o ./tmp/hanane.c ./tmp/hanane.ec}
-FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/hanane.lus
+PASS: ../utils/test_lus2lic_no_node should_work/hanane.lus
PASS: ./lus2lic {-2c should_work/hanane.lus -n hanane}
PASS: gcc hanane_hanane.c hanane_hanane_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/hanane.lus
+PASS: ../utils/compare_exec_and_2c should_work/hanane.lus
PASS: ./lus2lic {-o ./tmp/lustre.lic should_work/lustre.lus}
PASS: ./lus2lic {-ec -o ./tmp/lustre.ec should_work/lustre.lus}
PASS: ./myec2c {-o ./tmp/lustre.c ./tmp/lustre.ec}
@@ -1365,7 +1365,7 @@ PASS: ./myec2c {-o ./tmp/ck3.c ./tmp/ck3.ec}
PASS: ../utils/test_lus2lic_no_node should_work/ck3.lus
PASS: ./lus2lic {-2c should_work/ck3.lus -n ck3}
PASS: gcc ck3_ck3.c ck3_ck3_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/ck3.lus
+PASS: ../utils/compare_exec_and_2c should_work/ck3.lus
PASS: ./lus2lic {-o ./tmp/zzz.lic should_work/zzz.lus}
PASS: ./lus2lic {-ec -o ./tmp/zzz.ec should_work/zzz.lus}
PASS: ./myec2c {-o ./tmp/zzz.c ./tmp/zzz.ec}
@@ -1520,7 +1520,7 @@ PASS: ./myec2c {-o ./tmp/ck2.c ./tmp/ck2.ec}
PASS: ../utils/test_lus2lic_no_node should_work/ck2.lus
PASS: ./lus2lic {-2c should_work/ck2.lus -n ck2}
PASS: gcc ck2_ck2.c ck2_ck2_loop.c
-FAIL: Try to compare lus2lic -exec and -2c: ../utils/compare_exec_and_2c should_work/ck2.lus
+PASS: ../utils/compare_exec_and_2c should_work/ck2.lus
PASS: ./lus2lic {-o ./tmp/X.lic should_work/X.lus}
PASS: ./lus2lic {-ec -o ./tmp/X.ec should_work/X.lus}
PASS: ./myec2c {-o ./tmp/X.c ./tmp/X.ec}
@@ -1670,8 +1670,10 @@ XPASS: Test bad programs (semantics): lus2lic {-o ./tmp/bug.lic should_fail/sema
=== lus2lic Summary ===
-# of expected passes 1519
-# of unexpected failures 78
+# of expected passes 1532
+# of unexpected failures 65
# of unexpected successes 21
# of expected failures 37
# of unresolved testcases 3
+testcase ./lus2lic.tests/non-reg.exp completed in 263 seconds
+testcase ./lus2lic.tests/progression.exp completed in 0 seconds
diff --git a/test/lus2lic.time b/test/lus2lic.time
index 57344452..6ea332fa 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,2 +1,2 @@
-testcase ./lus2lic.tests/non-reg.exp completed in 262 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 263 seconds
testcase ./lus2lic.tests/progression.exp completed in 0 seconds
diff --git a/test/should_work/hanane.lus b/test/should_work/hanane.lus
index 8e8fd2af..b34c689f 100644
--- a/test/should_work/hanane.lus
+++ b/test/should_work/hanane.lus
@@ -24,7 +24,7 @@ var
h5: string2d^a when a1;
h6: string2d ;
let
- res = (h1[0]>1) when a1;
+ res = true -> (h1[0]>1) when a1;
h1 = current(if pre res then b1[1] else b1[2]);
h2 = current(c1);
h3 = c1[0].x + c1[1].z[2][1][0];
diff --git a/todo.org b/todo.org
index bea9953f..ccff6c89 100644
--- a/todo.org
+++ b/todo.org
@@ -18,7 +18,7 @@ http://www.di.ens.fr/~pouzet/bib/lctes12.pdf
** TODO lic2c : Ca plante si un identificateur lustre se nomme double...
- State "TODO" from "" [2014-06-13 Fri 16:59]
-** TODO lic2c : type externes utilisés en I/O du main pas supporté
+** TODO lic2c : types externes utilisés en I/O du main pas supportés
file:test/should_work/simple.lus lus2lic -2c should_work/simple.lus -n simple
types externes
@@ -72,62 +72,26 @@ et que ca marche tres bien. Ce qui prouve bien que ca ne sert a rien cette affai
grep "FAIL:" lus2lic.log | grep "exec" | grep "\-2c" | sed s/'FAIL: Try to compare lus2lic -exec and -2c:'/-/
-1. ../utils/compare_exec_and_2c should_work/ck5.lus
- -> erreur de clock !
-
-2. ../utils/compare_exec_and_2c should_work/test_node_expand2.lus
+1) ../utils/compare_exec_and_2c should_work/test_node_expand2.lus
-> -2110104000 est n'est pas un entier acceptable pour lutin sur les machines 32 bits...
-3. ../utils/compare_exec_and_2c should_work/test_node_expand.lus
+2) ../utils/compare_exec_and_2c should_work/test_node_expand.lus
-> idem
-4. ../utils/compare_exec_and_2c should_work/sincos.lus
+3) ../utils/compare_exec_and_2c should_work/sincos.lus
-> une erreur en mode -exec au step 2 (nil)
-5. ../utils/compare_exec_and_2c should_work/clock_ite.lus
- -> pb!
-
-6. ../utils/compare_exec_and_2c should_work/integrator.lus
+4) ../utils/compare_exec_and_2c should_work/integrator.lus
-> pb d'arrondi (1305025.02198 vs 1305025.)
-7. ../utils/compare_exec_and_2c should_work/PCOND1.lus
- -> pb d'arrondi / 32bits
-
-8. ../utils/compare_exec_and_2c should_work/CURRENT.lus
- -> manisfestement, le comportement du current diverge...
-
-9. ../utils/compare_exec_and_2c should_work/TIME_STABLE.lus
- -> pb!
-
-10. ../utils/compare_exec_and_2c should_work/multipar.lus
+5) ../utils/compare_exec_and_2c should_work/PCOND1.lus
-> pb d'arrondi / 32bits
-11. ../utils/compare_exec_and_2c should_work/bob.lus
- -> manisfestement, le comportement du current diverge...
-
-12. ../utils/compare_exec_and_2c should_work/test_condact.lus
- -> pb!
-
-13. ../utils/compare_exec_and_2c should_work/array_concat.lus
- -> le a.out fait un segmentation fault
-
-14. ../utils/compare_exec_and_2c should_work/ck4.lus
- -> manisfestement, le comportement du current diverge...
-
-15. ../utils/compare_exec_and_2c should_work/filliter.lus
- -> manisfestement, le comportement du current diverge...
+6) ../utils/compare_exec_and_2c should_work/multipar.lus
+ -> pb d'arrondi / 32bits
-16. ../utils/compare_exec_and_2c should_work/X2.lus
- -> pb!
-
-17. ../utils/compare_exec_and_2c should_work/hanane.lus
- -> manisfestement, le comportement du current diverge...
-
-18. ../utils/compare_exec_and_2c should_work/ck3.lus
- -> manisfestement, le comportement du current diverge...
-
-19. ../utils/compare_exec_and_2c should_work/ck2.lus
- -> manisfestement, le comportement du current diverge...
+7) ../utils/compare_exec_and_2c should_work/array_concat.lus
+ -> le a.out fait un segmentation fault
** TODO Divergences -exec et ecexe
@@ -139,23 +103,18 @@ grep "FAIL:" lus2lic.log | grep "exec" | grep "\-2c" | sed s/'FAIL: Try to compa
2. ../utils/test_lus2lic_no_node should_work/test_node_expand2.lus
3. ../utils/test_lus2lic_no_node should_work/test_node_expand.lus
4. ../utils/test_lus2lic_no_node should_work/modes3x2_v2.lus
-5. ../utils/test_lus2lic_no_node should_work/X6.lus
-6. ../utils/test_lus2lic_no_node should_work/filter.lus
-7. ../utils/test_lus2lic_no_node should_work/sincos.lus
-8. ../utils/test_lus2lic_no_node should_work/integrator.lus
-9. ../utils/test_lus2lic_no_node should_work/PCOND1.lus
-10. ../utils/test_lus2lic_no_node should_work/multiclock.lus
-11. ../utils/test_lus2lic_no_node should_work/multipar.lus
-12. ../utils/test_lus2lic_no_node should_work/activation2.lus
-13. ../utils/test_lus2lic_no_node should_work/bob.lus
-14. ../utils/test_lus2lic_no_node should_work/test_condact.lus
-15. ../utils/test_lus2lic_no_node should_work/activation1.lus
-16. ../utils/test_lus2lic_no_node should_work/Gyroscope.lus
-17. ../utils/test_lus2lic_no_node should_work/hanane.lus
-18. ../utils/test_lus2lic_no_node should_work/cond01.lus
-19. ../utils/test_lus2lic_no_node should_work/speedcontrol.lus
-20. ../utils/test_lus2lic_no_node should_work/PCOND.lus
-
+5. ../utils/test_lus2lic_no_node should_work/filter.lus
+6. ../utils/test_lus2lic_no_node should_work/sincos.lus
+7. ../utils/test_lus2lic_no_node should_work/integrator.lus
+8. ../utils/test_lus2lic_no_node should_work/PCOND1.lus
+9. ../utils/test_lus2lic_no_node should_work/multipar.lus
+10. ../utils/test_lus2lic_no_node should_work/activation2.lus
+11. ../utils/test_lus2lic_no_node should_work/bob.lus
+12. ../utils/test_lus2lic_no_node should_work/test_condact.lus
+13. ../utils/test_lus2lic_no_node should_work/activation1.lus
+14. ../utils/test_lus2lic_no_node should_work/Gyroscope.lus
+15. ../utils/test_lus2lic_no_node should_work/cond01.lus
+16. ../utils/test_lus2lic_no_node should_work/speedcontrol.lus
* Packages, modeles, etc.
** STARTED Il ne detecte plus les erreurs de type lors d'instanciation de noeuds
@@ -197,6 +156,8 @@ file:src/astInstanciateModel.ml
file:test/should_fail/type/parametric_node.lus
* Testing process
+** TODO Use severale machine to launch tests in paralell
+ - State "TODO" from "" [2014-08-14 Thu 11:23]
** TODO Testing node with enums don't work
- State "TODO" from "" [2013-05-28 Tue 14:46]
@@ -264,6 +225,28 @@ file:~/lus2lic/utils/test_lus2lic_no_node
- lus2lic -2c should_work/speedcontrol.lus -n speedcontrol
* Divers
+** TODO Traiter TOUS les warnings !!!
+ - State "TODO" from "" [2014-08-13 Wed 17:33]
+** TODO pb d'horloge
+ - State "TODO" from "" [2014-08-13 Wed 17:33]
+#+BEGIN_SRC lustre
+node xxx(x:int;c:bool) returns (res1,res2:int);
+var
+ y:int when c;
+ k:int when c;
+let
+ y = x when c;
+ k = (0 fby (k+1)) when c ;-- erreur ici, alors que ca semble bon
+ res1 = current(y);
+ res2 = current(k);
+tel
+#+END_SRC
+
+clock error: ' on c on base' is not a sub-clock of ' on base'
+en plus le message est bizzare
+
+** TODO Soc2cIdent.key_op2str est faux
+ - State "TODO" from "" [2014-08-13 Wed 17:33]
** TODO msg d'erreur un peu mauvais sur ce programme
#+begin_src lustre
--
GitLab