diff --git a/src/ast2lic.ml b/src/ast2lic.ml
index 751befc86e8be1273a3879f28e3b77bcb47fe9f8..ca73e51c163ed20aa05429b646015c580c8cd16f 100644
--- a/src/ast2lic.ml
+++ b/src/ast2lic.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 11/04/2013 (at 17:31) by Erwan Jahier> *)
+(* Time-stamp: <modified the 28/05/2013 (at 08:33) by Erwan Jahier> *)
open Lxm
@@ -292,7 +292,7 @@ and (of_eq: IdSolver.t -> AstCore.eq_info srcflagged -> Lic.eq_info srcflagged)
fun id_solver eq_info ->
let (lpl, ve) = eq_info.it in
let lpl_eff = List.map (translate_left_part id_solver) lpl
- and clk_subst,ve_eff = translate_val_exp id_solver UnifyClock.empty_subst ve
+ and clk_subst,ve_eff = translate_val_exp_check id_solver UnifyClock.empty_subst ve
in
type_check_equation id_solver eq_info.src lpl_eff ve_eff;
clock_check_equation id_solver eq_info.src clk_subst lpl_eff ve_eff;
@@ -343,6 +343,17 @@ and (translate_left_part : IdSolver.t -> AstCore.left_part -> Lic.left) =
| _ -> raise (Compile_error(sif.src, "an array was expected"))
)
+
+(* Translate and performs the checks *)
+and (translate_val_exp_check : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
+ -> UnifyClock.subst * Lic.val_exp) =
+ 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, _, s = EvalClock.f lxm id_solver s vef [] in
+ s, vef
+
and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
-> UnifyClock.subst * Lic.val_exp) =
fun id_solver s ve ->
@@ -420,7 +431,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
ve_typ = [Array_type_eff(List.hd (List.hd vel_eff).ve_typ, List.length vel_eff)];
ve_clk = (List.hd vel_eff).ve_clk
}
- in
+ in
CallByPosLic(flagit by_pos_op_eff lxm, [array_val_exp])
in
let s, vef_core =
@@ -434,11 +445,11 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
| Predef_n({it=ICONST_n i}) ->
s, mk_by_pos_op(Lic.CONST (Int_const_eff i))
| Predef_n({it=NOR_n;src=lxm}) -> s, mk_nary_pos_op(
- Lic.PREDEF_CALL (flagit (AstPredef.op_to_long NOR_n,[]) lxm))
+ Lic.PREDEF_CALL (flagit (AstPredef.op_to_long NOR_n,[]) lxm))
| Predef_n({it=DIESE_n;src=lxm}) -> s, mk_nary_pos_op(
- Lic.PREDEF_CALL (flagit (AstPredef.op_to_long DIESE_n,[]) lxm))
+ Lic.PREDEF_CALL (flagit (AstPredef.op_to_long DIESE_n,[]) lxm))
| Predef_n(op) -> s, mk_by_pos_op(
- Lic.PREDEF_CALL (flagit (AstPredef.op_to_long op.it,[]) op.src))
+ Lic.PREDEF_CALL (flagit (AstPredef.op_to_long op.it,[]) op.src))
| CALL_n node_exp_f ->
let neff = of_node id_solver node_exp_f in
let ceff = Lic.CALL (flagit neff.node_key_eff node_exp_f.src) in
@@ -497,10 +508,13 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
in
s, vef_core, lxm
in
- let vef, tl = EvalType.f id_solver { ve_core=vef_core; ve_typ=[]; ve_clk = [] } in
- let vef, _, s = EvalClock.f lxm id_solver s vef [] in
- s, vef
+ 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
)
+
+
and translate_by_name_op id_solver op s =
let to_long idref =
match Ident.pack_of_idref idref with
@@ -572,7 +586,7 @@ and (translate_slice_info : IdSolver.t -> AstCore.slice_info ->
let (of_assertion : IdSolver.t -> AstCore.val_exp Lxm.srcflagged ->
Lic.val_exp Lxm.srcflagged) =
fun id_solver vef ->
- let s, val_exp_eff = translate_val_exp id_solver UnifyClock.empty_subst vef.it in
+ let s, val_exp_eff = translate_val_exp_check id_solver UnifyClock.empty_subst vef.it in
(* Check that the assert is a bool. *)
let val_exp_eff, evaled_exp = EvalType.f id_solver val_exp_eff in
List.iter
diff --git a/src/compile.ml b/src/compile.ml
index bb6d4204a9c6bd675ec96424706ed4a2b8a546bf..0be76775b5156f5dedaef3dea7ef7703f67c802c 100644
--- a/src/compile.ml
+++ b/src/compile.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 26/04/2013 (at 17:45) by Erwan Jahier> *)
+(* Time-stamp: <modified the 24/05/2013 (at 17:44) by Erwan Jahier> *)
open Lxm
open Lv6errors
diff --git a/src/evalClock.ml b/src/evalClock.ml
index d67a1a0fb521f76436d02ade47ab37020fa7ad43..05bf0e84f5025383fede0e93057bfa780ee6bd51 100644
--- a/src/evalClock.ml
+++ b/src/evalClock.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 11/04/2013 (at 15:29) by Erwan Jahier> *)
+(* Time-stamp: <modified the 23/05/2013 (at 15:23) by Erwan Jahier> *)
open AstPredef
@@ -199,48 +199,62 @@ let rec (f : Lxm.t -> IdSolver.t -> subst -> Lic.val_exp -> Lic.clock list ->
print_string (
"Clocking the expression '" ^ (LicDump.string_of_val_exp_eff ve) ^"': "^
(LicDump.string_of_clock2 (List.hd clks)) ^"\n");
+ assert(ve.ve_clk <> []);
ve, inf_clks, s
-and f_aux id_solver s ve =
- let (cel, s), lxm =
- match ve.ve_core with
- | CallByPosLic ({it=posop; src=lxm}, args) ->
- eval_by_pos_clock id_solver posop lxm args s, lxm
- | CallByNameLic ({it=nmop; src=lxm}, nmargs ) -> (
- try eval_by_name_clock id_solver nmop lxm nmargs s, lxm
- with EvalConst_error msg ->
- raise (Compile_error(lxm, "\n*** can't eval constant: "^msg))
- )
- | Merge(ce, cl) ->
- let (merge_clk : Lic.clock) = List.hd ce.ve_clk in
- let ce_id,lxm = match ce with
- | { ve_core= CallByPosLic({it = VAR_REF id ; src = lxm },[]) } -> id,lxm
- | _ -> assert false
- in
- let check_case s (c,ve) =
- (* Check that ve is on c(ce) on merge_clk *)
- let id_clk =
- match c.it with
- | Bool_const_eff true -> "Lustre", "true"
- | Bool_const_eff false -> "Lustre", "false"
- | Enum_const_eff (s,_) -> s
- | _ -> assert false
+and (f_aux : IdSolver.t -> subst -> Lic.val_exp -> Lic.val_exp * Lic.id_clock list * subst) =
+ fun id_solver s ve ->
+ let ve, cel, s, lxm =
+ 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 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
+ )
+ | CallByNameLic ({it=nmop; src=lxm}, nmargs) -> (
+ try
+ let nmargs, cel, s = eval_by_name_clock id_solver nmop lxm nmargs s in
+ let ve = { ve with ve_core = CallByNameLic ({it=nmop; src=lxm}, nmargs) } in
+ List.iter (fun (_,arg) -> assert (arg.ve_clk <> [])) nmargs;
+ ve, cel, s, lxm
+ with EvalConst_error msg ->
+ raise (Compile_error(lxm, "\n*** can't eval constant: "^msg))
+ )
+ | Merge(ce, cl) ->
+ let ce, cel, s = f_aux id_solver s ce in
+ let (merge_clk : Lic.clock) = List.hd ce.ve_clk in
+ let ce_id,lxm = match ce with
+ | { ve_core= CallByPosLic({it = VAR_REF id ; src = lxm },[]) } -> id,lxm
+ | _ -> assert false
+ in
+ let check_case (s,acc) (c,ve) =
+ (* Check that ve is on c(ce) on merge_clk *)
+ let id_clk =
+ match c.it with
+ | Bool_const_eff true -> "Lustre", "true"
+ | Bool_const_eff false -> "Lustre", "false"
+ | Enum_const_eff (s,_) -> s
+ | _ -> assert false
+ in
+ let id_clk = (id_clk, ce_id, Lic.type_of_const c.it) in
+ let exp_clk = [On(id_clk, merge_clk)] in
+ let ve,cel,s = f c.src id_solver s ve exp_clk in
+ s, (c,ve)::acc
in
- let id_clk = (id_clk, ce_id, Lic.type_of_const c.it) in
- let exp_clk = [On(id_clk, merge_clk)] in
- let _ve,cel,s = f c.src id_solver s ve exp_clk in
- s
- in
- let s = List.fold_left check_case s cl in
- ([ce_id,merge_clk],s), lxm
- in
- 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
- s, ve
- in
- apply_subst_val_exp s ve, cel, s
+ let s,cl = List.fold_left check_case (s,[]) cl in
+ let ve = { ve with ve_core = Merge(ce, List.rev cl) } in
+ ve, [ce_id,merge_clk], s, lxm
+ in
+ 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
+ s, ve
+ in
+ let ve = apply_subst_val_exp s ve in
+ assert(ve.ve_clk <> []);
+ ve, cel, s
(* iterate f on a list of expressions *)
and (f_list : IdSolver.t -> subst -> Lic.val_exp list ->
@@ -254,161 +268,158 @@ and (f_list : IdSolver.t -> subst -> Lic.val_exp list ->
let args = List.rev args in
let cil = List.rev cil in
let cil = List.map (List.map(fun (id,clk) -> id, apply_subst2 s clk)) cil in
+ List.iter (fun arg -> assert (arg.ve_clk <> [])) args;
args, cil, s
and (eval_by_pos_clock : IdSolver.t -> Lic.by_pos_op -> Lxm.t -> Lic.val_exp list ->
- subst -> Lic.id_clock list * subst) =
+ subst -> Lic.val_exp list * Lic.id_clock list * subst) =
fun id_solver posop lxm args s ->
let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in
- 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
- let current_clock = function
- | (id, BaseLic) -> (id, BaseLic)
- | (id, On(_,clk)) -> (id, clk)
- | (_, ClockVar _) -> assert false
- in
- List.map current_clock (List.flatten clocks_of_args), s
- )
- | Lic.WHEN when_exp_clk,args -> (
- let c_clk =
- match when_exp_clk with
- | BaseLic -> BaseLic
- | ClockVar _ -> assert false
- | On((cc,c,_), c_clk) ->
-(* | NamedClock { it = (cc,c) ; src = lxm } -> *)
-(* let id, c_clk = (id_solver.id2var c lxm).var_clock_eff in *)
- c_clk
- in
- let aux_when exp_clk s =
- (*
- In order to clock check an expression such as
-
- exp when C(c)
-
- we first need to check that the clock of c (c_clk)
- is a sub-clock of the clock of exp (exp_clk).
- *)
+ 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
+ let current_clock = function
+ | (id, BaseLic) -> (id, BaseLic)
+ | (id, On(_,clk)) -> (id, clk)
+ | (_, ClockVar _) -> assert false
+ in
+ args, (List.map current_clock (List.flatten clocks_of_args), s)
+ )
+ | Lic.WHEN when_exp_clk,args -> (
+ let c_clk =
+ match when_exp_clk with
+ | BaseLic -> BaseLic
+ | ClockVar _ -> assert false
+ | On((cc,c,_), c_clk) ->
+ (* | NamedClock { it = (cc,c) ; src = lxm } -> *)
+ (* let id, c_clk = (id_solver.id2var c lxm).var_clock_eff in *)
+ c_clk
+ in
+ let aux_when exp_clk s =
+ (*
+ In order to clock check an expression such as
+
+ exp when C(c)
+
+ we first need to check that the clock of c (c_clk)
+ is a sub-clock of the clock of exp (exp_clk).
+ *)
+ match is_a_sub_clock lxm s exp_clk (fst exp_clk,c_clk) with
+ | None ->
+ let msg = "\n*** clock error: '" ^ (ci2str (snd exp_clk)) ^
+ "' is not a sub-clock of '" ^ (ci2str c_clk) ^ "'"
+ in
+ raise (Compile_error(lxm, msg))
+ | Some s ->
+ let id_when_exp_clk, s =
+ match exp_clk with
+ | id, On(var, _) -> (id, when_exp_clk), s
+ | id, BaseLic -> (id, when_exp_clk), s
+ | id, ClockVar i ->
+ let id_when_exp_clk = id, when_exp_clk in
+ let (s1,s2) = s in
+ id_when_exp_clk,
+ (s1, UnifyClock.add_subst2 i when_exp_clk s2)
+ in
+ id_when_exp_clk, s
+ in
+ (match f_list id_solver s args with
+ (* XXX ce cas ne sert à rien !!!
+ le traitement du cas ou la liste ne contient qu'un element
+ n'a aucun raison d'etre particulier, si ???
+ *)
+ | args,[[exp_clk]], s ->
+ let (exp_clk,s) = aux_when exp_clk s in
+ args,([exp_clk], s)
+
+ | args, [exp_clk_list], s ->
+ (* when on tuples *)
+ let exp_clk_list, s =
+ List.fold_left
+ (fun (acc,s) exp_clk ->
+ let (exp_clk,s) = aux_when exp_clk s in
+ exp_clk::acc, s
+ )
+ ([],s)
+ exp_clk_list
+ in
+ args,(List.rev exp_clk_list, s)
+ | _ -> assert false (* "(x1,x2) when node (x,y)" *)
+ )
+ )
+ | Lic.HAT(i), ve::_ ->
+ let (ve,clk,s) = f_aux id_solver s ve in
+ [ve],(clk,s)
- match is_a_sub_clock lxm s exp_clk (fst exp_clk,c_clk) with
- | None ->
- let msg = "\n*** clock error: '" ^ (ci2str (snd exp_clk)) ^
- "' is not a sub-clock of '" ^ (ci2str c_clk) ^ "'"
- in
- raise (Compile_error(lxm, msg))
- | Some s ->
- let id_when_exp_clk, s =
- match exp_clk with
- | id, On(var, _) -> (id, when_exp_clk), s
- | id, BaseLic -> (id, when_exp_clk), s
- | id, ClockVar i ->
- let id_when_exp_clk = id, when_exp_clk in
- let (s1,s2) = s in
- id_when_exp_clk,
- (s1, UnifyClock.add_subst2 i when_exp_clk s2)
- in
- id_when_exp_clk, s
- in
- (match f_list id_solver s args with
- (* XXX ce cas ne sert à rien !!!
- le traitement du cas ou la liste ne contient qu'un element
- n'a aucun raison d'etre particulier, si ???
- *)
- | _args,[[exp_clk]], s ->
- let (exp_clk,s) = aux_when exp_clk s in
- ([exp_clk], s)
-
- | _args, [exp_clk_list], s ->
- (* when on tuples *)
- let exp_clk_list, s =
- List.fold_left
- (fun (acc,s) exp_clk ->
- let (exp_clk,s) = aux_when exp_clk s in
- exp_clk::acc, s
- )
- ([],s)
- exp_clk_list
- in
- (List.rev exp_clk_list, s)
- | _ -> assert false (* "(x1,x2) when node (x,y)" *)
+ | Lic.VAR_REF id,args ->
+ let vi = IdSolver.var_info_of_ident id_solver id lxm in
+ args,([var_info_eff_to_clock_eff vi], s)
+
+ | Lic.CONST c, args -> (
+ let s, clk = UnifyClock.new_clock_var s in
+ args,([Lic.string_of_const c, clk], s)
)
- )
-
- (* f_aux id_solver (List.hd args) *)
-
- | Lic.HAT(i),[ve] ->
- let (_,clk,s) = f_aux id_solver s ve in
- clk,s
- | Lic.HAT(i),_ -> assert false
-
- | Lic.VAR_REF id,args ->
- let vi = IdSolver.var_info_of_ident id_solver id lxm in
- ([var_info_eff_to_clock_eff vi], s)
-
- | Lic.CONST c, args -> (
- let s, clk = UnifyClock.new_clock_var s in
- [Lic.string_of_const c, clk], s
- )
- | Lic.CONST_REF idl,args ->
- let _const = IdSolver.const_eff_of_item_key id_solver idl lxm in
- let s, clk = UnifyClock.new_clock_var s in
- ([Ident.of_long idl, clk], s)
- | Lic.CALL nkf,args ->
- let node_key = nkf.it in
- let node_exp_eff = IdSolver.node_exp_of_node_key id_solver node_key lxm in
- let (cil_arg, cil_res) = get_clock_profile node_exp_eff 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.
-
- Hence we create a fresh var clock, that will be instanciated
- by the caller.
- *)
- let (replace_base : Lic.clock -> Lic.id_clock -> Lic.id_clock) =
- fun rel_base (id,ci) ->
- (* [replace_base rel_base ci ] replaces in [ci] any occurences of the
- base clock by [rel_base] *)
- let rec aux ci =
- match ci with
- | BaseLic -> rel_base
- | On(v,clk) -> On(v, aux clk)
- | ClockVar i -> ci
- in
- id, aux ci
- in
- let cil_arg = List.map (replace_base rel_base) cil_arg in
- let cil_res = List.map (replace_base rel_base) cil_res in
- let args, clk_args, s = f_list id_solver s args in
- let s = check_args lxm s cil_arg (List.flatten clk_args) in
- List.map (apply_subst s) cil_res, s
-
- | Lic.PREDEF_CALL (nkf),args ->
- let op = AstPredef.string_to_op (snd(fst nkf.it)) in
- let args, clk_args, s = f_list id_solver s args in
- let flat_clk_args = List.flatten clk_args in (* all predef nodes are mono-clock! *)
- let _,flat_clk_args = List.split flat_clk_args in
- let clk_list, s =
- if args = [] then [],s else
- let _clk,s = UnifyClock.list lxm flat_clk_args s in
- List.map (List.map (apply_subst s)) clk_args, s
- in
- LicEvalClock.f id_solver op lxm s clk_list
-
- (* One argument. *)
- | Lic.PRE,args
- | Lic.STRUCT_ACCESS _,args
- | Lic.ARRAY_ACCES (_),args
- | Lic.ARRAY_SLICE (_),args ->
- assert(List.length args = 1);
- let (_,clk,s) = f_aux id_solver s (List.hd args) in
- clk,s
-
- (* may have tuples as arguments *)
- | Lic.TUPLE,args
- | Lic.ARROW,args
- | Lic.FBY ,args
- | Lic.CONCAT,args
- | Lic.ARRAY,args -> (
+ | Lic.CONST_REF idl,args ->
+ let _const = IdSolver.const_eff_of_item_key id_solver idl lxm in
+ let s, clk = UnifyClock.new_clock_var s in
+ args,([Ident.of_long idl, clk], s)
+ | Lic.CALL nkf,args ->
+ let node_key = nkf.it in
+ let node_exp_eff = IdSolver.node_exp_of_node_key id_solver node_key lxm in
+ let (cil_arg, cil_res) = get_clock_profile node_exp_eff 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.
+
+ Hence we create a fresh var clock, that will be instanciated
+ by the caller.
+ *)
+ let (replace_base : Lic.clock -> Lic.id_clock -> Lic.id_clock) =
+ fun rel_base (id,ci) ->
+ (* [replace_base rel_base ci ] replaces in [ci] any occurences of the
+ base clock by [rel_base] *)
+ let rec aux ci =
+ match ci with
+ | BaseLic -> rel_base
+ | On(v,clk) -> On(v, aux clk)
+ | ClockVar i -> ci
+ in
+ id, aux ci
+ in
+ let cil_arg = List.map (replace_base rel_base) cil_arg in
+ let cil_res = List.map (replace_base rel_base) cil_res in
+ let args, clk_args, s = f_list id_solver s args in
+ let s = check_args lxm s cil_arg (List.flatten clk_args) in
+ args, (List.map (apply_subst s) cil_res, s)
+
+ | Lic.PREDEF_CALL (nkf),args ->
+ let op = AstPredef.string_to_op (snd(fst nkf.it)) in
+ let args, clk_args, s = f_list id_solver s args in
+ let flat_clk_args = List.flatten clk_args in (* all predef nodes are mono-clock! *)
+ let _,flat_clk_args = List.split flat_clk_args in
+ let clk_list, s =
+ if args = [] then [],s else
+ let _clk,s = UnifyClock.list lxm flat_clk_args s in
+ List.map (List.map (apply_subst s)) clk_args, s
+ in
+ args, LicEvalClock.f id_solver op lxm s clk_list
+
+ (* One argument. *)
+ | Lic.PRE,args
+ | Lic.STRUCT_ACCESS _,args
+ | Lic.ARRAY_ACCES (_),args
+ | Lic.ARRAY_SLICE (_),args ->
+ assert(List.length args = 1);
+ let (arg,clk,s) = f_aux id_solver s (List.hd args) in
+ [arg], (clk,s)
+
+ (* may have tuples as arguments *)
+ | Lic.TUPLE,args
+ | Lic.ARROW,args
+ | Lic.FBY ,args
+ | Lic.CONCAT,args
+ | Lic.ARRAY,args -> (
(* Check that all args are of the same (unifiable) clocks.
XXX : we suppose that all those operators are
@@ -426,24 +437,27 @@ and (eval_by_pos_clock : IdSolver.t -> Lic.by_pos_op -> Lxm.t -> Lic.val_exp lis
List.combine idl clk_l
| _ -> List.map (apply_subst s) (List.hd clk_args)
in
- clk_list, s
- )
+ args, (clk_list, s)
+ )
+ in
+ args, cl, s
and (eval_by_name_clock : IdSolver.t -> Lic.by_name_op -> Lxm.t ->
(Ident.t Lxm.srcflagged * Lic.val_exp) list -> subst ->
- Lic.id_clock list * subst) =
+ (Ident.t Lxm.srcflagged * Lic.val_exp) list * Lic.id_clock list * subst) =
fun id_solver namop lxm namargs s ->
let apply_subst s (id,clk) = id, UnifyClock.apply_subst s clk in
let args = List.map (fun (id,ve) -> ve) namargs in
(* XXX The 3 following lines duplicates the code of TUPLE_eff and co *)
let args, clk_args, s = f_list id_solver s args in
+ let namargs = List.map2 (fun (id,_ve) ve -> id,ve) namargs args in
let flat_clk_args = List.flatten clk_args in (* => mono-clock! *)
let _,flat_clk_args = List.split flat_clk_args in
let clk,s = UnifyClock.list lxm flat_clk_args s in
let clk_list = List.map (apply_subst s) (List.hd clk_args) in
match namop with
| Lic.STRUCT_anonymous -> assert false (* cf EvalType.E *)
- | Lic.STRUCT(_) -> clk_list, s
+ | Lic.STRUCT(_) -> namargs, clk_list, s
| Lic.STRUCT_with(_, dft) ->
(* XXX should i do something here ??? *)
- clk_list, s
+ namargs,clk_list, s
diff --git a/src/l2lExpandArrays.ml b/src/l2lExpandArrays.ml
index 01713ff7e657545413d9a5acc135aa86b1a00b0b..ba9d642b55b38c8cb7d5860ae77cc7632a0c4f8c 100644
--- a/src/l2lExpandArrays.ml
+++ b/src/l2lExpandArrays.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 26/04/2013 (at 17:34) by Erwan Jahier> *)
+(** Time-stamp: <modified the 27/05/2013 (at 16:23) 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...
@@ -67,8 +67,10 @@ let new_var str lctx type_eff clock_eff =
*)
exception Polymorphic
+
(* returns a new var based on [vi] with type [type_eff]. *)
let clone_var node_env vi str type_eff =
+
let str = (Ident.to_string vi.var_name_eff) ^ str in
let id = Ident.of_string (str) in
let clk_id = Ident.of_string str in
@@ -217,6 +219,7 @@ let (expand_left : local_ctx -> left -> left list) =
in
flatten_var_tree vt
+
(********************************************************************************)
(** build a new loc that will alias ve, and add its definition in the
set of equations (cf acc) *)
@@ -330,7 +333,7 @@ and do_const acc lctx lxm const =
let ve_const,acc =
match ve_const.ve_core with
| CallByPosLic ({it=CONST_REF _},_) ->
- (* in order to avoid a potential infinite loop *)
+ (* in order to avoid a potential infinite loop *)
(ve_const, acc)
| _ -> expand_val_exp lctx acc ve_const
@@ -342,78 +345,78 @@ and (break_tuple : Lxm.t -> left list -> val_exp -> Lic.eq_info srcflagged list)
(* 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)
- | CallByPosLic ({it= ARRAY}, vel) -> List.flatten (List.map aux vel)
- | CallByPosLic ({src=lxm;it= HAT(i)}, vel) ->
- let ve1 = List.hd vel in
- let ve1l = aux ve1 in
- List.map
- (fun ve1 -> { ve1 with ve_core = CallByPosLic ({src=lxm;it= HAT(i)}, [ve1])} )
+ let rec aux ve = (* flatten val exp*)
+ match ve.ve_core with
+ | CallByPosLic ({it= TUPLE}, vel)
+ | CallByPosLic ({it= ARRAY}, vel) -> List.flatten (List.map aux vel)
+ | CallByPosLic ({src=lxm;it= HAT(i)}, vel) ->
+ let ve1 = List.hd vel in
+ let ve1l = aux ve1 in
+ List.map
+ (fun ve1 -> { ve1 with ve_core = CallByPosLic ({src=lxm;it= HAT(i)}, [ve1])} )
+ ve1l
+ | CallByPosLic (unop, [ve1]) ->
+ let ve1l = aux ve1 in
+ List.map
+ (fun ve1 -> { ve1 with ve_core = CallByPosLic (unop, [ve1])} )
+ ve1l
+ | CallByPosLic (binop, [ve1;ve2]) ->
+ let ve1l, ve2l = aux ve1, aux ve2 in
+ if (List.length ve1l <> List.length ve2l) then
+ let vel2str vel =
+ (String.concat ", " (List.map LicDump.string_of_val_exp_eff vel))
+ in
+ let msg =
+ "*** error expression " ^ (LicDump.string_of_val_exp_eff ve) ^
+ "\n cannot be broken \n" ^(vel2str ve1l) ^
+ " should have the same arity as\n"^(vel2str ve2l) ^ "\n"
+ in
+ raise (Lv6errors.Compile_error(lxm, msg))
+ else
+ List.map2
+ (fun ve1 ve2 ->
+ { ve with ve_core = CallByPosLic (binop, [ve1;ve2])})
ve1l
- | CallByPosLic (unop, [ve1]) ->
- let ve1l = aux ve1 in
- List.map
- (fun ve1 -> { ve1 with ve_core = CallByPosLic (unop, [ve1])} )
+ ve2l
+ | CallByPosLic ({it= PREDEF_CALL(
+ {src=if_lxm ; it = ("Lustre","if"),[]}); src=lxm}, [cond; ve1; ve2]) -> (
+ let ve1l, ve2l = aux ve1, aux ve2 in
+ if (List.length ve1l <> List.length ve2l) then
+ let vel2str vel =
+ (String.concat ", " (List.map LicDump.string_of_val_exp_eff vel))
+ in
+ let msg =
+ "*** error expression " ^ (LicDump.string_of_val_exp_eff ve) ^
+ "\n cannot be broken \n" ^(vel2str ve1l) ^
+ " should have the same arity as\n"^(vel2str ve2l) ^ "\n"
+ in
+ raise (Lv6errors.Compile_error(lxm, msg))
+ else
+ List.map2
+ (fun ve1 ve2 ->
+ { ve with ve_core =
+ CallByPosLic ({it= PREDEF_CALL({src=if_lxm ; it = ("Lustre","if"),[]}); src=lxm},
+ [cond;ve1;ve2])}
+ )
ve1l
- | CallByPosLic (binop, [ve1;ve2]) ->
- let ve1l, ve2l = aux ve1, aux ve2 in
- if (List.length ve1l <> List.length ve2l) then
- let vel2str vel =
- (String.concat ", " (List.map LicDump.string_of_val_exp_eff vel))
- in
- let msg =
- "*** error expression " ^ (LicDump.string_of_val_exp_eff ve) ^
- "\n cannot be broken \n" ^(vel2str ve1l) ^
- " should have the same arity as\n"^(vel2str ve2l) ^ "\n"
- in
- raise (Lv6errors.Compile_error(lxm, msg))
- else
- List.map2
- (fun ve1 ve2 ->
- { ve with ve_core = CallByPosLic (binop, [ve1;ve2])})
- ve1l
- ve2l
- | CallByPosLic ({it= PREDEF_CALL(
- {src=if_lxm ; it = ("Lustre","if"),[]}); src=lxm}, [cond; ve1; ve2]) -> (
- let ve1l, ve2l = aux ve1, aux ve2 in
- if (List.length ve1l <> List.length ve2l) then
- let vel2str vel =
- (String.concat ", " (List.map LicDump.string_of_val_exp_eff vel))
- in
- let msg =
- "*** error expression " ^ (LicDump.string_of_val_exp_eff ve) ^
- "\n cannot be broken \n" ^(vel2str ve1l) ^
- " should have the same arity as\n"^(vel2str ve2l) ^ "\n"
- in
- raise (Lv6errors.Compile_error(lxm, msg))
- else
- List.map2
- (fun ve1 ve2 ->
- { ve with ve_core =
- CallByPosLic ({it= PREDEF_CALL({src=if_lxm ; it = ("Lustre","if"),[]}); src=lxm},
- [cond;ve1;ve2])}
- )
- ve1l
- ve2l
- )
- | _ -> [ve]
- in
- let vel = aux ve in
- if (List.length vel <> List.length left_list) then
+ ve2l
+ )
+ | _ -> [ve]
+ in
+ let vel = aux ve in
+ if (List.length vel <> List.length left_list) 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) =
@@ -549,7 +552,7 @@ and (expand_var_info: local_ctx -> var_info list * acc ->
(vil, acc)
fl
| Array_type_eff(at,size) -> (
- let rec aux i (vil,acc) =
+ let rec local_aux i (vil,acc) =
if i=size then (vil,acc) else
let new_var = clone_var lctx vi ("_" ^ soi i) at in
let new_vil, new_acc = expand_var_info lctx (vil,acc) new_var in
@@ -559,9 +562,9 @@ and (expand_var_info: local_ctx -> var_info list * acc ->
(* XXX
Hashtbl.add nenv.lenv_vars new_var.var_name_eff new_var *)
);
- aux (i+1) (new_vil, new_acc)
+ local_aux (i+1) (new_vil, new_acc)
in
- aux 0 (vil,acc)
+ local_aux 0 (vil,acc)
)
| External_type_eff(_)
| Enum_type_eff (_, _)
@@ -570,7 +573,8 @@ and (expand_var_info: local_ctx -> var_info list * acc ->
| Bool_type_eff ->
vi::vil, acc
in
- aux vi.var_type_eff
+ let vil,acc = aux vi.var_type_eff in
+ vil,acc
let rec (node : local_ctx -> Lic.node_exp -> Lic.node_exp) =
fun lctx n ->
diff --git a/src/l2lSplit.ml b/src/l2lSplit.ml
index 43dfb5d6a03a1f976535bb74fa7a55320d412595..a840593dd69dca45550df8cadcaf0abe8c8c673c 100644
--- a/src/l2lSplit.ml
+++ b/src/l2lSplit.ml
@@ -190,14 +190,14 @@ and (split_val_exp : bool -> bool -> LicPrg.id_generator -> Lic.val_exp ->
| CallByPosLic({src=lxm;it=Lic.CONST _}, _)
-> if not when_flag then
let clk = ve.ve_clk in
- match (List.hd clk) with
- | On(clock,clk) ->
+ match (clk) with
+ | On(clock,clk)::_ ->
{ ve with ve_core =
CallByPosLic({src=lxm;it=Lic.WHEN(On(clock,clk))},[ve])},
- ([],[])
-
- | (ClockVar _) (* should not occur *)
- | BaseLic -> ve, ([],[])
+ ([],[])
+ | (ClockVar _)::_ (* should not occur *)
+ | BaseLic::_ -> ve, ([],[])
+ | [] -> assert false (* should not occur *)
else
ve, ([],[])
| CallByNameLic (by_name_op_eff, fl) -> (
diff --git a/src/main.ml b/src/main.ml
index 00b272ded085636d64d9851805320bea5e196979..2ba7e7995a8c5e31a106445e721985cd9fd0902c 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 14/05/2013 (at 14:43) by Erwan Jahier> *)
+(* Time-stamp: <modified the 27/05/2013 (at 16:53) by Erwan Jahier> *)
open Verbose
open AstV6
diff --git a/src/rif_base.ml b/src/rif_base.ml
index e33b12d0d23e231cbb72af54fcd973afac1bb5cf..1523506e6af97bafa60e4c4d0813cecdca0106a5 100644
--- a/src/rif_base.ml
+++ b/src/rif_base.ml
@@ -159,6 +159,8 @@ and (parse_rif_stream : in_channel -> out_channel option -> vntl -> stream ->
parse_rif_stream ic oc
vntl (get_stream ic oc) tbl pragma
)
+ | (Genlex.Kwd (_,"#"))::(Genlex.Kwd (_,"ERROR"))::_ ->
+ print_string "#ERROR value read. bye!\n"; raise Bye
| (Genlex.Kwd (_,"#"))::_ ->
Stream.junk stream ;
parse_rif_stream ic oc vntl (get_stream ic oc)
diff --git a/src/socExec.ml b/src/socExec.ml
index 6767850e8dbdfdb921cabe49ae55bca33a063708..e615acf51dcfe27b45e1cb3ec0dd16caa2116559 100644
--- a/src/socExec.ml
+++ b/src/socExec.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 14/05/2013 (at 16:01) by Erwan Jahier> *)
+(* Time-stamp: <modified the 24/05/2013 (at 09:55) by Erwan Jahier> *)
open Soc
open Data
@@ -172,7 +172,7 @@ and (filter_params : Soc.t -> Soc.var list -> int list -> Soc.var list) =
fun soc el il ->
let local_nth i l =
try List.nth l i
- with _ ->
+ with _ ->
print_string (
"\n*** Cannot get the " ^ (string_of_int (i+1)) ^
"the element of a list of size " ^ (string_of_int (List.length l))^"\n");
diff --git a/src/unifyClock.ml b/src/unifyClock.ml
index 9ebe034979f578e7eb2a9d5172aae771c75e6837..9ea09ee5abda07f8c1a83f9ead8aed6763eb5bea 100644
--- a/src/unifyClock.ml
+++ b/src/unifyClock.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 11/04/2013 (at 15:32) by Erwan Jahier> *)
+(* Time-stamp: <modified the 23/05/2013 (at 09:29) by Erwan Jahier> *)
open LicDump
@@ -339,5 +339,3 @@ let rec (const_to_val_eff: Lxm.t -> bool -> subst -> const -> subst * val_exp) =
ve_typ = [stype] ;
ve_clk = [BaseLic]
}
-
-
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index 0e225769d65bae948fb9f1b1d5baea43f3733876..f60fe0f1420d9489205caab85bc02f790be0e338 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Wed May 22 14:36:57 2013
+Test Run By jahier on Tue May 28 08:35:55 2013
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
@@ -1044,5 +1044,3 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
# of unexpected successes 12
# of expected failures 37
# of unresolved testcases 20
-testcase ./lus2lic.tests/non-reg.exp completed in 417 seconds
-testcase ./lus2lic.tests/progression.exp completed in 0 seconds
diff --git a/test/lus2lic.time b/test/lus2lic.time
index cbc6a24265b9cb623ed829b5f626207c732a4104..f7d006663b6e568c4e23a849b22785ba5e474122 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,2 +1,2 @@
-testcase ./lus2lic.tests/non-reg.exp completed in 417 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 335 seconds
testcase ./lus2lic.tests/progression.exp completed in 0 seconds
diff --git a/test/site.exp b/test/site.exp
index a4d838a51ff19607d3c4450bd312ac5332cb6b32..ad96852976064ae6738d9ff55b33ae8f5f8d581c 100644
--- a/test/site.exp
+++ b/test/site.exp
@@ -104,6 +104,7 @@ proc should_fail { test_name fail_kind command_line args } {
}
timeout {
unresolved "Time out $test_name ($fail_kind): $cl $args"
+ exit
}
}
return $spawn_id
diff --git a/todo.org b/todo.org
index 28d567aac39b03d45ed3a8d9862e1dc764c92c3e..a8d6ff83f20e30cd28e77a6f94b34cef164eadfe 100644
--- a/todo.org
+++ b/todo.org
@@ -135,6 +135,7 @@ file:test/should_fail/type/parametric_node.lus
- State "TODO" from "" [2013-01-18 Fri 23:12]
in particular, are nodes using extern nodes generated properly?
+
** TODO les (nouveaux) tests ne capturent pas les changements de # lignes dans les should_fail
- State "TODO" from "" [2013-01-11 Fri 11:15]
@@ -144,6 +145,7 @@ in particular, are nodes using extern nodes generated properly?
#+begin_src sh
./lus2lic _assertion_oracle.lus -n assertion_oracle -en -esa
+#+end_src
*** Error in file "/home/jahier/lus2lic/test/_assertion_oracle.lus", line 38, col 3 to 7, token 'v02_1':
***
@@ -211,7 +213,6 @@ en fait, quand ecexe se plante (oracle), il bloque tout le monde...
../utils/test_lus2lic_no_node should_work/onlyroll2.lus
../utils/test_lus2lic_no_node should_work/integrator.lus
../utils/test_lus2lic_no_node should_work/over2.lus
-../utils/test_lus2lic_no_node should_work/left.lus
* Divers
diff --git a/utils/test_lus2lic_no_node b/utils/test_lus2lic_no_node
index 4a9b3790a697ce0db185a7d109d585d45c24c1e5..de5b65403783ef3c0bab46c2bdf52d8017b45668 100755
--- a/utils/test_lus2lic_no_node
+++ b/utils/test_lus2lic_no_node
@@ -24,9 +24,9 @@ cat $lustre_file >> $_oracle;
if
-./lus2lic $_oracle -n $oracle -lv4 -eei -en --no-prefix -o lv4$_oracle;
+ ./lus2lic $_oracle -n $oracle -lv4 -eei -en --no-prefix -o lv4$_oracle;
then
-echo "lus2lic -lv4 done"
+ echo "lus2lic -lv4 done"
else
echo "Error"
exit 2
@@ -35,10 +35,11 @@ fi
export PATH=/usr/local/tools/lustre/bin/:$PATH
if
+# ./lus2lic $_oracle -n $oracle -ec -o $oracle.ec
./lus2lic lv4$_oracle -n $oracle -ec -o $oracle.ec
# lus2ec $_oracle $oracle -o $oracle.ec;
then
-echo "pollux done"
+echo "ec generation done"
else
echo "Error"
exit 2
@@ -51,4 +52,4 @@ else
echo "error"
exit 2
fi
-#exit 0
+exit 0