From 5dd64311d97f066f50dabd98cb2aad20703cd07f Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Thu, 26 Jun 2008 16:02:42 +0200
Subject: [PATCH] A new implementation of EvalClock, that is more general.
Not yet implemented (assert false): iterators, struct
Add a UnifyClock module, and rename Unify into UnifyType.
nb : a lot of test are now broken, because
- the clock checking is now plugged ;-)
- iterators, struct are not yet implemented
---
src/Makefile | 6 +-
src/TODO | 13 +-
src/evalClock.ml | 537 ++--
src/evalClock.mli | 11 +-
src/evalType.ml | 18 +-
src/getEff.ml | 10 +-
src/lazyCompiler.ml | 10 +-
src/main.ml | 4 +-
src/predefEvalType.ml | 8 +-
src/predefSemantics.ml | 8 +-
src/test/should_work/NONREG/PCOND.lus | 11 +-
src/test/should_work/NONREG/Watch.lus | 9 +-
src/test/should_work/call/bad_call02.lus | 2 +-
src/test/should_work/clock/clock.lus | 37 +-
src/test/should_work/packEnvTest/Condact.lus | 2 +-
src/test/test.res.exp | 2784 +-----------------
src/unifyClock.ml | 119 +
src/unifyClock.mli | 48 +
src/{unify.ml => unifyType.ml} | 7 +-
src/{unify.mli => unifyType.mli} | 0
src/uniqueOutput.ml | 12 +-
src/uniqueOutput.mli | 4 +-
22 files changed, 659 insertions(+), 3001 deletions(-)
create mode 100644 src/unifyClock.ml
create mode 100644 src/unifyClock.mli
rename src/{unify.ml => unifyType.ml} (97%)
rename src/{unify.mli => unifyType.mli} (100%)
diff --git a/src/Makefile b/src/Makefile
index e5f82a44..5b96be8e 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -34,8 +34,10 @@ SOURCES = \
./symbolTab.ml \
./compiledData.ml \
./compiledDataDump.ml \
- ./unify.mli \
- ./unify.ml \
+ ./unifyType.mli \
+ ./unifyType.ml \
+ ./unifyClock.mli \
+ ./unifyClock.ml \
./syntaxTab.mli \
./syntaxTab.ml \
./predefEvalType.mli \
diff --git a/src/TODO b/src/TODO
index 9513cb9a..87b4e682 100644
--- a/src/TODO
+++ b/src/TODO
@@ -90,6 +90,11 @@ les operateurs aritmetiques, bof.
* autoriser les noeuds (ou fonction) sans corps sans avoir a préciser
"extern" ?
+* accepter les tuples multi-horloges ? ca parait logique, a partir du
+ moment où on accepte les noeuds multi-horloges. De même, la " -> "
+ devrait être multi-horloge également. Et peut-etre d'autres encore...
+
+
***********************************************************************************
***********************************************************************************
*** questions pour bibi
@@ -138,11 +143,11 @@ n'est pas le cas pour l'instant...
*** facile
-* Pb des noms de modules
- ../lus2lic should_work/NONREG/dependeur_struct.lus
- ->
+* ../lus2lic should_work/NONREG/Int.lus
- ../lus2lic should_work/NONREG/Int.lus
+ "zero" versus "Int::zero". Ce probleme est une consequence d'un
+ mauvaix choid de représentation pour les ident dans l'abre
+ syntaxique. cf le laius a propos de solveIdent.ml plus bas.
* dans evalType, je ne checke pas tous les arguments !
ecrire les tests idoines puis faire ces checks.
diff --git a/src/evalClock.ml b/src/evalClock.ml
index 40d80c63..05120596 100644
--- a/src/evalClock.ml
+++ b/src/evalClock.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 16/06/2008 (at 15:26) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/06/2008 (at 16:00) by Erwan Jahier> *)
open Predef
@@ -10,7 +10,7 @@ open CompiledDataDump
open Printf
open Lxm
open Errors
-
+open UnifyClock
(** clock checking of expression.
@@ -21,7 +21,6 @@ open Errors
- other kind of expressions can be seen as nodes, as they «take» some input
arguments, and return some outputs.
-
The clock checking consists in verifying that expression arguments clocks
are compatible with the expression parameters clocks.
@@ -39,252 +38,144 @@ open Errors
- the result clocks are ok, i.e., v2 is on v1 + v1 is on v3 (2)
cf the [check_res] function below
- Let's focus first on argument checking:
-*)
-type clock_info_par =
- | Base_par of var_info_eff
- | Input_par of var_info_eff * int
- | Output_par of var_info_eff * int
+** Checking expression arguments
+--------------------------------
-(** A [clock_info_par] is an abstraction of a [var_info_eff] meant to
- be able to check the clocks of expressions arguments. A pair of
- list of [clock_info_par] is therefore represent the expression
- clock profile.
+ ok. So now, let us detail how we clock check expression arguments.
+ e.g., in the equation
- In this abstraction, the name binding is replaced by a relative
- position binding.
+ (x,y)=toto(a,b);
- For instance, for a node toto of profile:
-
- node toto(a; b when a) returns (x when a; y when x);
+ we want to make sure that the clocks of the argument "a" and "b" are compatible
+ with the input clock profile of "toto".
- we have as input profile: [Base_arg; Input_par 0]
- and as output profile: [Input_par 0, Output_par 0]
-
- This information is extracted from the node profile by
- [get_clock_profile]:
-*)
+ To do that, we suppose we have already computed:
-type clock_profile = clock_info_par list * clock_info_par list
+ - "cil_par" the expected input clock profile (via "get_clock_profile")
+ - "cil_arg" the list of clocks of arguments (via a rec call to f)
-let (get_clock_profile : Lxm.t -> node_exp_eff -> clock_profile) =
- fun lxm n ->
- let (il, ol) = (n.inlist_eff, n.outlist_eff) in
- let rec find_index v l i =
- match l with
- | [] -> raise Not_found
- | v2::tail -> if v=v2 then i else find_index v tail (i+1)
- in
- let f v =
- match v.var_clock_eff with
- | BaseEff -> Base_par(v)
- | On clk ->
- try Input_par(v, find_index clk il 0)
- with Not_found ->
- try Output_par(v, find_index clk ol 0)
- with Not_found ->
- let msg = "\n*** "^ (Ident.to_string clk.var_name_eff)^
- ": unknown clock" in
- raise(Compile_error (lxm, msg))
- in
- (List.map f il, List.map f ol)
-
-(** We also introduce a second kind of var_info_eff abstraction, dedicated
- to the checking of expresion result:
+ In order to check that this call is correct, we check that both
+ terms are unifiable.
*)
-type clock_info_res =
- | Base_res of var_info_eff
- | OnVar of var_info_eff * var_info_eff
- | OnRel of var_info_eff * int
-let string_of_clock_info_res = function
- | Base_res v -> (Ident.to_string v.var_name_eff) ^ " on base"
- | OnVar (v,clk) -> (Ident.to_string v.var_name_eff) ^ " on " ^
- (Ident.to_string clk.var_name_eff)
- | OnRel (v,i) -> (Ident.to_string v.var_name_eff) ^ " on #" ^
- (string_of_int i) ^ "^nth"
-(** For example, when checking the equation
+let (check_args : Lxm.t -> subst -> clock_info list -> clock_info list -> subst) =
+ fun lxm s cil_par cil_arg ->
+ assert (List.length cil_par = List.length cil_arg);
+ let s = List.fold_left2 (UnifyClock.f lxm) s cil_par cil_arg in
+ s
- (x,y)=toto(a,b);
-
- the clock checking of "toto(a,b)" will return
- [OnVar a, OnRel 0]
- which makes it easy to compute that:
- - x is on a,
- - y is on x
-
- Hence, [clock_info_res list] is the type that is return by f, the
- main function of this clock checking module.
-
+(** Checking expression result
+ --------------------------
- ** Checking expression arguments
- --------------------------------
+ It is the same thing, except that we have left_eff list instead
+ of clock_info list.
- ok. So now, let us detail how we clock check expression
- arguments. e.g., in the equation
+ e.g., in the equation:
(x,y)=toto(a,b);
- we want to make sure that the clocks of the argument "a" and "b" are compatible
- with the input clock profile of "toto".
-
- To do that, we suppose we have already computed:
-
- - "ci_par_l" the expected input clock profile (via "get_clock_profile" defined
- above)
- - "cl" the list of arguments "clock_info_res" (via a rec call to f)
-*)
-let (check_args : Lxm.t -> clock_info_par list -> clock_info_res list -> unit) =
- fun lxm ci_par_l cl ->
- let (f : clock_info_par -> clock_info_res -> unit) =
- fun cip cir -> match (cip,cir) with
- | Base_par _, Base_res _ -> ()
- | Input_par(vpar,i), OnRel (v,j) -> if i = j then () else
- let msg = "\n*** clock error" in
- raise(Compile_error(lxm,msg))
-
- | Input_par(vpar,i), OnVar (v,clk) ->
- (match List.nth cl i with
- | OnVar (v2,clk2) ->
- if clk2 = clk then () else
- let msg = "\n*** clock error: " ^
- (string_of_clock_info_res (OnVar (v,clk))) ^ " (provided) <> " ^
- (string_of_clock_info_res (OnVar (v2,clk2))) ^ " (expected)"
- in
- raise(Compile_error(lxm, msg))
- | Base_res(v2) ->
- let msg = "\n*** clock error: " ^
- (string_of_clock_info_res (OnVar (v,clk))) ^ " (provided) <> " ^
- "base (expected)"
- in
- raise(Compile_error(lxm,msg))
- | OnRel (v,i) -> assert false
- )
- | Input_par _, Base_res(_)
- | Base_par _, _ ->
- raise(Compile_error(lxm,"\n*** clock error: bad arg clocks"))
- | Output_par _, _ -> assert false (* inputs cannot be clocked on outputs*)
- in
- List.iter2 f ci_par_l cl
-
-(** In order to use check_args, we need another intermediary function
- that merges list of list of [clock_info_res]. Indeed, to be able
- to check the arguments of an expression like:
-
- tata(toto(a,b),toto(c,d));
-
- We sais before that we compute the [clock_info_res list] of the
- arguments via a recursive call to f. But such a recursive call
- returns a list of list of [clock_info_res], which contains
- information relative to variable positions. Therefore we cannot
- just flatten that list of list; we also need to shift the indexes
- encoding variable positions.
-
- For example, for checking the args of tata above, we call
+ we want to check that the clocks of "x" and "y" are compatible with
+ the output clock profile of node "toto".
- merge_clock_ll [[OnVar a; OnRel 0]; [OnVar c; OnRel 0]]
+ To do that, we suppose we have:
- that ougth to return the following flattenned list with shifted index:
-
- [OnVar a; OnRel 0; OnVar c; OnRel 2]
+ - "left" the list of left_eff
+ - "rigth" the list of result clock. (via "get_clock_profile" again)
- and then we can call check_res with that list.
+ and we just need to check that both side are unifiable.
*)
-let (merge_clock_ll: clock_info_res list list -> clock_info_res list) =
- fun ll ->
- let f (shift,acc) l =
- let new_l = List.map
- (function
- | Base_res(v) -> Base_res(v)
- | OnVar(v,clk) -> OnVar(v,clk)
- | OnRel(v,j) -> OnRel(v,j+shift)
- )
- l
+let rec (var_info_eff_of_left_eff: left_eff -> var_info_eff) =
+ function
+ | LeftVarEff (v, _) -> v
+ | LeftFieldEff (l, id,_) ->
+ let v = var_info_eff_of_left_eff l in
+ let new_name = (Ident.to_string v.var_name_eff) ^ "." ^ (Ident.to_string id) in
+ { v with var_name_eff = Ident.of_string new_name }
+
+ | LeftArrayEff (l,i,_) ->
+ let v = var_info_eff_of_left_eff l in
+ let new_name = (Ident.to_string v.var_name_eff) ^ "[" ^
+ (string_of_int i) ^ "]"
in
- (shift + (List.length l), acc @ new_l)
- in
- snd (List.fold_left f (0,[]) ll)
-
+ { v with var_name_eff = Ident.of_string new_name }
+ | LeftSliceEff (l,si,_) ->
+ let v = var_info_eff_of_left_eff l in
+ let new_name = (Ident.to_string v.var_name_eff) ^ (string_of_slice_info_eff si)
+ in
+ { v with var_name_eff = Ident.of_string new_name }
-(** Checking expression result
- --------------------------
- e.g., in the equation:
+(* exported *)
+let (check_res : Lxm.t -> subst -> left_eff list -> clock_info list -> unit) =
+ fun lxm s left rigth ->
+ let left_vi = List.map var_info_eff_of_left_eff left in
+ let left_ci = List.map var_info_eff_to_clock_info left_vi in
+ if (List.length left_ci <> List.length rigth) then
+ raise (Compile_error(lxm, "!!!"));
+ ignore(List.fold_left2 (UnifyClock.f lxm) s left_ci rigth)
- (x,y)=toto(a,b);
- we want to check that the clocks of "x" and "y" are compatible with
- the output clock profile of node "toto".
-
- To do that, we suppose we have already computed:
+(******************************************************************************)
+(** Now we can go on and define [f]. *)
- - "cil" the expected output clock profile (via "get_clock_profile" again)
- - "cel" the list of result "clock_info_res"
+(** 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))
*)
-let (check_res2 : Lxm.t -> clock_info_res list -> clock_info_res list -> unit) =
- fun lxm cil cel ->
- if cil = cel then () else
- let msg = "\n*** clock error: " ^
- (String.concat ", " (List.map string_of_clock_info_res cil)) ^ " <> " ^
- (String.concat ", " (List.map string_of_clock_info_res cel))
- in
- raise(Compile_error(lxm,msg))
-
-let (get_nth_var : clock_info_res list -> int -> var_info_eff) =
- fun vil i ->
- match List.nth vil i with
- | Base_res(v) -> v
- | OnVar(v,_) -> v
- | OnRel(v,_) -> v
-
-let (check_res : Lxm.t -> clock_info_res list -> clock_eff list -> unit) =
- fun lxm rigth left ->
- let cpt = ref 0 in
- let (f : clock_info_res -> clock_eff -> unit) =
- fun cip ce ->
- incr cpt;
- match (cip,ce) with
- | Base_res(_), BaseEff -> ()
- | OnVar(v1,clk1), On clk2 ->
- if clk1 = clk2 then () else
- let msg = "\n*** clock error (ckeck_res), " ^
- (string_of_int !cpt) ^ "nth element:"^
- (Ident.to_string clk2.var_name_eff) ^ " <> " ^
- (Ident.to_string clk1.var_name_eff)
- in
- raise(Compile_error(lxm,msg))
-
- | OnRel(v,i), On clk ->
- let clk2 = get_nth_var rigth i in
- if clk2 = clk then () else
- let msg = "\n*** clock error (ckeck_res), " ^
- (string_of_int !cpt) ^ "nth element:"^
- (Ident.to_string clk.var_name_eff) ^ " <> " ^
- (Ident.to_string clk2.var_name_eff)
- in
- raise(Compile_error(lxm,msg))
-
-
- | Base_res _, On _
- | _, BaseEff -> raise(Compile_error(lxm,"\n*** clock error"))
- in
- if List.length rigth <> List.length left then
- raise(Compile_error(lxm,"\n*** clock error"))
- else
- List.iter2 f rigth left
+let rec (is_a_sub_clock : Lxm.t -> subst -> clock_info -> clock_info -> subst option) =
+ fun lxm s sc c ->
+ (* check if [sc] is a sub-clock of [c] (in the large
+ sens). Returns Some updated substitution if it is the case,
+ and None otherwise *)
+ match sc,c with
+ (* the base clock is a sub-clock of all clocks *)
+ | Ci_base, (Ci_base|Ci_on(_,_)|Ci_var _) -> Some s
+
+ | Ci_on(v,clk), Ci_base -> None
+ | Ci_on(v,clk), Ci_on(v2,clk2) -> (
+ try Some(UnifyClock.f lxm s clk clk2)
+ with _ -> is_a_sub_clock lxm s sc clk2
+ )
+ | Ci_var j, Ci_base -> assert false
+ | Ci_var i, Ci_on(_,_)
+ | Ci_var i, Ci_var _ ->
+ (* XXX can it occur? if yes, something should be done
+ the problem being that several things are possible
+ (there is no unique sub-clock of a clock...
+ Well, ok, let's suppose that they are equal for the time being,
+ which seems wrong in the general case.
+ *)
+ let s1,s2 = s in
+ Some (s1,(i,c)::s2)
+ | Ci_on(_,_), Ci_var i -> (* Ditto *)
+ let s1,s2 = s in
+ Some (s1,(i,sc)::s2)
-(** Now we can go on and define [f]. *)
+
+type clock_profile = clock_info list * clock_info list
+
+let (get_clock_profile : node_exp_eff -> clock_profile) =
+ fun n ->
+ (List.map var_info_eff_to_clock_info n.inlist_eff,
+ List.map var_info_eff_to_clock_info n.outlist_eff)
+
+let ci2str = string_of_clock_info
(******************************************************************************)
+(* Stuff to generated fresh var clocks *)
+
+let var_type = ref 0
+let reset_var_type () = var_type := 0
+let get_var_type () = incr var_type; !var_type
let cpt_var_name = ref 0
+
let (make_dummy_var: string -> var_info_eff) =
fun str ->
let id = Ident.of_string (str ^ (string_of_int !cpt_var_name)) in
@@ -296,91 +187,171 @@ let (make_dummy_var: string -> var_info_eff) =
var_clock_eff = BaseEff;
}
+let get_constant_clock () = Ci_var (get_var_type ())
+(* Ci_on(make_dummy_var "const",Ci_var (get_var_type ())) *)
+
+let concat_subst (s11,s12) (s21,s22) = (s11 @ s21, s12@s22)
+
+(******************************************************************************)
-let rec (f : id_solver -> val_exp_eff -> clock_info_res list) =
- fun id_solver ve ->
+let rec (f : id_solver -> subst -> val_exp_eff -> clock_info list * subst) =
+ fun id_solver s ve ->
cpt_var_name := 0;
- match ve with
- | CallByPosEff ({it=posop; src=lxm}, OperEff args) -> (
- eval_by_pos_clock id_solver posop lxm args
- )
- | CallByNameEff ({it=nmop; src=lxm}, nmargs ) ->
- try eval_by_name_clock id_solver nmop lxm nmargs
- with EvalConst_error msg ->
- raise (Compile_error(lxm, "\n*** can't eval constant: "^msg))
-
-and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list
- -> clock_info_res list) =
- fun id_solver posop lxm args ->
+ reset_var_type ();
+ (* we split f in into two so that we can reinit the fresh clock var generator *)
+ f_aux id_solver s ve
+
+and f_aux id_solver s ve =
+ match ve with
+ | CallByPosEff ({it=posop; src=lxm}, OperEff args) ->
+ eval_by_pos_clock id_solver posop lxm args s
+
+ | CallByNameEff ({it=nmop; src=lxm}, nmargs ) ->
+ try eval_by_name_clock id_solver nmop lxm nmargs s
+ with EvalConst_error msg ->
+ raise (Compile_error(lxm, "\n*** can't eval constant: "^msg))
+
+
+(* iterate f on a list of expression *)
+and (f_list : id_solver -> subst -> val_exp_eff list -> clock_info list list * subst) =
+ fun id_solver s args ->
+ let aux (acc,s) arg =
+ let cil, s = f_aux id_solver s arg in
+ (cil::acc, s)
+ in
+ let (cil, s) = List.fold_left aux ([],s) args in
+ List.rev cil, s
+
+and (eval_by_pos_clock : id_solver -> by_pos_op_eff -> Lxm.t -> val_exp_eff list ->
+ subst -> clock_info list * subst) =
+ fun id_solver posop lxm args s ->
match posop with
- | CALL_eff node_exp_eff ->
- let (ip,op) = get_clock_profile node_exp_eff.src node_exp_eff.it in
- let clocks_of_args = merge_clock_ll (List.map (f id_solver) args) in
- let res =
- List.map
- (function
- | Base_par(v) -> Base_res(v)
- | Output_par(v, i) -> OnRel(v, i)
- | Input_par(v, i) ->
- (* that would occur if one writes
- toto(tata(x),x)
- where one output clock of tata depends on one of its input, eg
-
- node tata(i) returns (o when i)
-
- arg...
- *)
- let msg = "\n*** clock error: this kind of expression can "^
- "not be clocked with our current algo, sorry..." in
- raise (Compile_error(lxm,msg))
+ | CURRENT_eff -> ( (* we return the clock of the argument *)
+ let clocks_of_args, s = f_list id_solver s args in
+ match List.flatten clocks_of_args with
+ | [Ci_base] -> [Ci_base],s
+ | [Ci_on(_,clk)] -> [clk],s
+ | _ -> assert false
+ )
+ | WHEN_eff -> (
+ match f_list id_solver s args with
+ | [[c1];[c2]], s -> (
+ (* c1 and c2 ougth to be on the same clock *)
+(* let c1 = apply_subst s c1 in *)
+(* let c2 = apply_subst s c2 in *)
+ match is_a_sub_clock lxm s c1 c2 with
+ | None ->
+ let msg = "\n*** clock error: '" ^ (ci2str (c1)) ^
+ "' is not a sub-clock of '" ^ (ci2str (c2)) ^ "'"
+ in
+ raise (Compile_error(lxm, msg))
+ | Some s ->
+ (match (List.hd (List.tl args)) with
+ | CallByPosEff({it=IDENT_eff id2; src=lxm2}, _) ->
+ let clk_var =
+ try (id_solver.id2var id2 lxm2)
+ with _ -> assert false
+ in
+ let clk = var_info_eff_to_clock_info clk_var in
+ let clk_of_c1,s =
+ match c1 with
+ | Ci_base -> assert false
+ | Ci_on(var,_) -> Ci_on(var, clk), s
+ | Ci_var i ->
+ let cc1 = Ci_on(make_dummy_var "const",clk) in
+ let (s1,s2) = s in
+ cc1, (s1,(i,cc1)::s2)
+ in
+ ([clk_of_c1], s)
+ | _ -> assert false)
)
- op
- in
- check_args lxm ip clocks_of_args;
- res
-
+ | [c1;[c2]], s -> assert false (* "(x1,x2) when v" *)
+ | _ -> assert false (* "(x1,x2) when node (x,y)" *)
+ )
+ | MERGE_eff _ -> assert false
+ (* f_aux id_solver (List.hd args) *)
+
+ | HAT_eff(i,ve) -> f_aux id_solver s ve
+ (* nb: the args have been put inside the HAT_eff constructor *)
+
+ | Predef_eff (ICONST_n _,_)
+ | Predef_eff (RCONST_n _,_)
+ | Predef_eff (TRUE_n,_)
+ | Predef_eff (FALSE_n,_) -> [get_constant_clock ()],s
+ | IDENT_eff idref -> (
+ try ([var_info_eff_to_clock_info (id_solver.id2var idref lxm)], s)
+ with _ -> (* => it is a constant *) [get_constant_clock ()],s
+ )
+ | CALL_eff node_exp_eff ->
+ let (cil_arg, cil_res) = get_clock_profile node_exp_eff.it in
+ (* the value of the base clock of a node is actually relative
+ to the context into which the node is called.
- | CURRENT_eff -> assert false (* prendre l'horloge de l'horloge de l'argument *)
-
- | WHEN_eff ->
- let clk_exp = List.nth args 1 in
- (* Non: je doit plutot extraire de clk_exp une var_info_eff,
- et raler si ca n'est pas possible.
+ Hence we create a fresh var clock, that will be instanciated
+ by the caller.
*)
- (f id_solver clk_exp)
-
-
- | MERGE_eff _ -> f id_solver (List.hd args)
+ let rel_base = Ci_var (get_var_type ()) in
+ let rec (replace_base : clock_info -> clock_info -> clock_info) =
+ fun rel_base ci ->
+ (* [replace_base rel_base ci ] replaces in [ci] any occurences of the
+ base clock by [rel_base] *)
+ match ci with
+ | Ci_base -> rel_base
+ | Ci_on(v,clk) -> Ci_on(v, replace_base rel_base clk)
+ | Ci_var i -> 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 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
- | Predef_eff (_,_)
- | WITH_eff
- | ARROW_eff
- | FBY_eff
- | CONCAT_eff
- | HAT_eff(_,_)
+ (* One argument. *)
| PRE_eff
| STRUCT_ACCESS_eff _
| ARRAY_ACCES_eff (_, _)
- | ARRAY_SLICE_eff (_,_)
+ | ARRAY_SLICE_eff (_,_) ->
+ assert(List.length args = 1);
+ f_aux id_solver s (List.hd args)
+
+ (* may have tuples as arguments *)
+ | TUPLE_eff
+ | Predef_eff (_,_)
+ | ARROW_eff
+ | FBY_eff
+ | WITH_eff
+ | CONCAT_eff
| ARRAY_eff -> (
- (* check that args are of the same clocks, which also is the
- returned clock *)
- match List.flatten (List.map (f id_solver) args) with
- | clk1::tail ->
- if List.for_all (fun clk -> clk = clk1) tail then [clk1] else
- raise (Compile_error(lxm, "clock mismatch"))
- | [] -> assert false
+ (* Check that all args are of the same (unifiable) clocks.
+
+ XXX : we suppose that all those operators are
+ mono-clocks (i.e., when they return tuples, all elements
+ are on the same clock). It would be sensible to have,
+ e.g., arrows on multiple clocks. We'll refine later. *)
+ let clk_args, s = f_list id_solver s args in
+ let flat_clk_args = List.flatten clk_args in (* => mono-clock! *)
+ let clk,s = UnifyClock.list lxm flat_clk_args s in
+ let clk_list =
+ match posop with
+ | TUPLE_eff -> List.map (apply_subst s) flat_clk_args
+
+ | Predef_eff (IF_n,[]) ->
+ (* for ite, the arity of the result is not the arity of
+ the condition *)
+ List.map (apply_subst s) (List.hd (List.tl clk_args))
+
+ | Predef_eff ((Map|Fill|Red|FillRed|BoolRed), sarg) ->
+ assert false
+ (* TODO *)
+
+ | _ -> List.map (apply_subst s) (List.hd clk_args)
+ in
+ clk_list, s
)
- | TUPLE_eff -> List.flatten (List.map (f id_solver) args)
-
-
- | IDENT_eff idref -> [Base_res(make_dummy_var (Ident.string_of_idref idref))]
- (* all constants are on the base clock *)
-
-
and (eval_by_name_clock : id_solver -> by_name_op_eff -> Lxm.t ->
- (Ident.t Lxm.srcflagged * val_exp_eff) list -> clock_info_res list) =
+ (Ident.t Lxm.srcflagged * val_exp_eff) list -> subst ->
+ clock_info list * subst) =
fun id_solver namop lxm namargs ->
match namop with
| STRUCT_anonymous_eff -> assert false (* cf EvalClock.f *)
diff --git a/src/evalClock.mli b/src/evalClock.mli
index d911f3f3..14bc8c64 100644
--- a/src/evalClock.mli
+++ b/src/evalClock.mli
@@ -1,17 +1,15 @@
-(** Time-stamp: <modified the 12/06/2008 (at 09:50) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/06/2008 (at 14:59) by Erwan Jahier> *)
open CompiledData
-
+open UnifyClock
(** [f ids ve ]checks that [ve] is well-clocked (i.e., for node calls,
it checks that the argument and the parameter clocks are correct),
and returns a clock profile that contains all the necessary information
to be able to check.
*)
+val f : id_solver -> subst -> val_exp_eff -> clock_info list * subst
-type clock_info_res
-
-val f : id_solver -> val_exp_eff -> clock_info_res list
(** [check_res lxm cel cil] check that the expected output clock
profile of an expression "cil" is compatible with the result clocks
@@ -31,5 +29,4 @@ val f : id_solver -> val_exp_eff -> clock_info_res list
*)
-val check_res : Lxm.t -> clock_info_res list -> clock_eff list -> unit
-val merge_clock_ll: clock_info_res list list -> clock_info_res list
+val check_res : Lxm.t -> subst -> left_eff list -> clock_info list -> unit
diff --git a/src/evalType.ml b/src/evalType.ml
index 21613165..8201b1aa 100644
--- a/src/evalType.ml
+++ b/src/evalType.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 14:47) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/06/2008 (at 14:49) by Erwan Jahier> *)
open Predef
@@ -43,10 +43,10 @@ and (eval_by_pos_type :
"\n*** arity error: %d argument(s) are expected, whereas %d is/are provided"
llti lt_args))
else
- (match Unify.f lti t_args with
- | Unify.Equal -> lto
- | Unify.Unif subst -> List.map (Unify.subst_type subst) lto
- | Unify.Ko msg -> raise (Compile_error(lxm, msg))
+ (match UnifyType.f lti t_args with
+ | UnifyType.Equal -> lto
+ | UnifyType.Unif subst -> List.map (UnifyType.subst_type subst) lto
+ | UnifyType.Ko msg -> raise (Compile_error(lxm, msg))
)
| IDENT_eff id -> (
@@ -75,10 +75,10 @@ and (eval_by_pos_type :
match List.map (f id_solver) args with
| [[Array_type_eff (teff0, size0)]; [Array_type_eff (teff1, size1)]] ->
let teff =
- match Unify.f [teff0] [teff1] with
- | Unify.Equal -> teff1
- | Unify.Unif subst -> Unify.subst_type subst teff1
- | Unify.Ko msg -> raise (Compile_error(lxm, msg))
+ match UnifyType.f [teff0] [teff1] with
+ | UnifyType.Equal -> teff1
+ | UnifyType.Unif subst -> UnifyType.subst_type subst teff1
+ | UnifyType.Ko msg -> raise (Compile_error(lxm, msg))
in
[Array_type_eff (teff, size0+size1)]
| _ ->
diff --git a/src/getEff.ml b/src/getEff.ml
index 6b1270ef..82d3550b 100644
--- a/src/getEff.ml
+++ b/src/getEff.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 16/06/2008 (at 15:44) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/06/2008 (at 15:01) by Erwan Jahier> *)
open Lxm
@@ -73,9 +73,9 @@ and (type_check_equation: id_solver -> eq_info srcflagged -> left_eff list ->
and (clock_check_equation:id_solver -> eq_info srcflagged -> left_eff list ->
val_exp_eff -> unit) =
fun id_solver eq_info lpl_eff ve_eff ->
-(* let right_part,s = EvalClock.f id_solver EvalClock.empty_subst ve_eff in *)
-(* EvalClock.check_res eq_info.src s lpl_eff right_part *)
- assert false
+ let right_part,s = EvalClock.f id_solver UnifyClock.empty_subst ve_eff in
+ EvalClock.check_res eq_info.src s lpl_eff right_part
+
(******************************************************************************)
let (get_static_params_from_idref : SymbolTab.t -> Lxm.t -> Ident.idref ->
@@ -176,7 +176,7 @@ and (eq : id_solver -> eq_info srcflagged -> eq_info_eff srcflagged) =
and ve_eff = translate_val_exp id_solver ve
in
type_check_equation id_solver eq_info lpl_eff ve_eff;
-(* clock_check_equation id_solver eq_info lpl_eff ve_eff; *)
+ clock_check_equation id_solver eq_info lpl_eff ve_eff;
flagit (lpl_eff, ve_eff) eq_info.src
diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml
index 6844c872..c4b27260 100644
--- a/src/lazyCompiler.ml
+++ b/src/lazyCompiler.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 17/06/2008 (at 15:22) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/06/2008 (at 14:49) by Erwan Jahier> *)
open Lxm
@@ -743,11 +743,11 @@ and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t ->
in
let (il,ol) = CompiledData.profile_of_node_exp_eff alias_node in
let (il_exp, ol_exp) = List.map aux vi_il, List.map aux vi_ol in
- match Unify.f il_exp il with
- | Unify.Ko msg -> raise(Compile_error(lxm, msg))
+ match UnifyType.f il_exp il with
+ | UnifyType.Ko msg -> raise(Compile_error(lxm, msg))
| _ ->
- match Unify.f ol_exp ol with
- | Unify.Ko msg -> raise(Compile_error (lxm, msg))
+ match UnifyType.f ol_exp ol with
+ | UnifyType.Ko msg -> raise(Compile_error (lxm, msg))
| _ ->
alias_node
)
diff --git a/src/main.ml b/src/main.ml
index bf68eaf2..6786f057 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 03/06/2008 (at 10:16) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/06/2008 (at 14:49) by Erwan Jahier> *)
(** Here follows a description of the different modules used by this lus2lic compiler.
@@ -221,7 +221,7 @@ let main = (
(* Compile.init_appli () ; *)
parse_args ();
if !Global.run_unit_test then (
- Unify.unit_test ()
+ UnifyType.unit_test ()
);
if (!Global.infiles = []) then (
Arg.usage arg_list usage_msg ;
diff --git a/src/predefEvalType.ml b/src/predefEvalType.ml
index 6c9d127d..022a4aff 100644
--- a/src/predefEvalType.ml
+++ b/src/predefEvalType.ml
@@ -1,11 +1,11 @@
-(** Time-stamp: <modified the 10/06/2008 (at 10:48) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/06/2008 (at 14:49) by Erwan Jahier> *)
open Predef
open SyntaxTreeCore
open CompiledData
open Lxm
open Errors
-open Unify
+open UnifyType
(* exported *)
@@ -117,7 +117,7 @@ let fillred_profile =
let (id1, t1) = List.hd lti and (id2, t2) = List.hd lto in
if t1 = t2 then (lti,lto) else
(* if they are not equal, they migth be unifiable *)
- match Unify.f [t1] [t2] with
+ match UnifyType.f [t1] [t2] with
| Equal -> (lti,lto)
| Unif t -> (List.map (fun (id,tid) -> id, subst_type t tid) lti,
List.map (fun (id,tid) -> id, subst_type t tid) lto)
@@ -269,7 +269,7 @@ let (f : op -> Lxm.t -> CompiledData.static_arg_eff list -> typer) =
if (List.length l <> List.length lti) then
arity_error [l] (string_of_int (List.length lti))
else
- match Unify.f lti l with
+ match UnifyType.f lti l with
| Equal -> lto
| Unif Any ->
type_error2
diff --git a/src/predefSemantics.ml b/src/predefSemantics.ml
index 6f10ce6f..8660a096 100644
--- a/src/predefSemantics.ml
+++ b/src/predefSemantics.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 10:04) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/06/2008 (at 14:49) by Erwan Jahier> *)
open Predef
@@ -6,7 +6,7 @@ open SyntaxTreeCore
open CompiledData
open Lxm
open Errors
-open Unify
+open UnifyType
(* exported *)
type typer = type_eff Predef.evaluator
@@ -137,7 +137,7 @@ let fillred_profile =
let (id1, t1) = List.hd lti and (id2, t2) = List.hd lto in
if t1 = t2 then (lti,lto) else
(* if they are not equal, they migth be unifiable *)
- match Unify.f [t1] [t2] with
+ match UnifyType.f [t1] [t2] with
| Equal -> (lti,lto)
| Unif t -> (List.map (fun (id,tid) -> id, subst_type_ext t tid) lti,
List.map (fun (id,tid) -> id, subst_type_ext t tid) lto)
@@ -281,7 +281,7 @@ let (type_eval : op -> Lxm.t -> CompiledData.static_arg_eff list -> typer) =
if (List.length l <> List.length lti) then
arity_error l (string_of_int (List.length lti))
else
- match Unify.f lti l with
+ match UnifyType.f lti l with
| Equal -> List.map type_eff_to_type_eff lto
| Unif Any ->
type_error2
diff --git a/src/test/should_work/NONREG/PCOND.lus b/src/test/should_work/NONREG/PCOND.lus
index a11cffdb..ff9f4b82 100644
--- a/src/test/should_work/NONREG/PCOND.lus
+++ b/src/test/should_work/NONREG/PCOND.lus
@@ -9,8 +9,13 @@ node PCOND(
returns (hX:bool when h0; X:int when hX);
let
hX = hC and current(hD) and ( ( hA and
-current(current(D)) ) or ( hB and not
-current(current(D)) ) );
+ current(current(D)) )
+ or
+ ( hB and not
+ current(current(D)) ) );
+
X = ( if ( hA and current(current(D)) )
-then current(A) else current(B) ) when hX;
+ then current(A)
+ else current(B)
+ ) when hX;
tel
diff --git a/src/test/should_work/NONREG/Watch.lus b/src/test/should_work/NONREG/Watch.lus
index 554dc7b2..5b457644 100644
--- a/src/test/should_work/NONREG/Watch.lus
+++ b/src/test/should_work/NONREG/Watch.lus
@@ -487,7 +487,7 @@ node DIVIDE (scale:int)
var n:int;
let
(n,quotient) = (0,true) -> (if ((pre(n) + 1) = scale) then (0,true)
- else (pre(n)+1,false));
+ else ((pre(n)+1),false));
tel
@@ -552,8 +552,9 @@ let
set_watch, set_alarm,
start_stop, lap, stop_alarm_beep) = BUTTONS(UPLEFT,LOWLEFT,UPRIGHT,LOWRIGHT);
- second = time_unit and (current(DIVIDE(TIME_SCALE(0) when time_unit)));--(true->time_unit))));
- -- converts the time unit (assumed to be the 1/TIME_SCALE(0)
- -- sec.) into the second
+ second = time_unit and (current(DIVIDE(TIME_SCALE(0) when time_unit)));
+ --(true->time_unit))));
+ -- converts the time unit (assumed to be the 1/TIME_SCALE(0)
+ -- sec.) into the second
tel
diff --git a/src/test/should_work/call/bad_call02.lus b/src/test/should_work/call/bad_call02.lus
index b92dab22..7f232733 100644
--- a/src/test/should_work/call/bad_call02.lus
+++ b/src/test/should_work/call/bad_call02.lus
@@ -1,7 +1,7 @@
-- clock checking of predefined ops
-node bad_call02(a:int; c:bool) returns (x : int);
+node bad_call02(a:int; c:bool) returns (x : int when c);
let
x = a when c;
tel
diff --git a/src/test/should_work/clock/clock.lus b/src/test/should_work/clock/clock.lus
index 19628523..f300f2cf 100644
--- a/src/test/should_work/clock/clock.lus
+++ b/src/test/should_work/clock/clock.lus
@@ -1,13 +1,4 @@
--- Entree sur entree: ok
-extern node clock2(clock2_u: bool; clock2_v: bool when clock2_u) returns (clock2_y: bool );
-
--- Sortie sur sortie: ok
-extern node clock3(clock3_u: bool) returns (clock3_toto: bool; clock3_y: bool when clock3_toto);
-
-
--- Entree sur entree et sortie sur sortie: ok
-extern node clock4(clock4_u: bool; clock4_v: bool when clock4_u) returns (clock4_x: bool; clock4_y: bool when clock4_x);
type s = struct {x: bool^10; y: bool};
@@ -15,10 +6,11 @@ type s = struct {x: bool^10; y: bool};
node clock(a: bool; b: bool) returns (c: bool; d: bool when c);
var
z: bool;
--- z2: bool;
+ z2: bool;
x: bool when z;
-- y: bool when x;
--- e : bool when b;
+ e : bool when a;
+-- f : bool when e;
let
-- c = clock2(a, (b or b) when a) or (true->a);
@@ -30,11 +22,28 @@ let
-- (z, x) = clock3(current(z when z2));
(z, x) = clock3(z);-- ok
-
+ e = b when a;
+-- f = a when e;
+
+
+
(c, d) = clock4(a, b when a);
-- z = clock5(a, b when a, e when a);
--- z2 = clock5(a, b when a, e when b when c);
+ z2 = clock5(a, b when a, c when e);
tel
+-- Entree sur entree: ok
+extern node clock2(clock2_u: bool; clock2_v: bool when clock2_u)
+returns (clock2_y: bool);
+
+-- Sortie sur sortie: ok
+extern node clock3(clock3_u: bool)
+returns (clock3_toto: bool; clock3_y: bool when clock3_toto);
+
+-- Entree sur entree et sortie sur sortie: ok
+extern node clock4(clock4_u: bool; clock4_v: bool when clock4_u)
+returns (clock4_x: bool; clock4_y: bool when clock4_x);
-extern node clock5(x : bool; y: bool when x; z: bool when y) returns (a: bool);
+--
+extern node clock5(x : bool; y: bool when x; z: bool when y)
+returns (a: bool);
diff --git a/src/test/should_work/packEnvTest/Condact.lus b/src/test/should_work/packEnvTest/Condact.lus
index 533fb6d6..d7c75765 100644
--- a/src/test/should_work/packEnvTest/Condact.lus
+++ b/src/test/should_work/packEnvTest/Condact.lus
@@ -32,7 +32,7 @@ model Condact
body
node C(c: bool; d: t2; x: t1) returns (y: t2);
let
- y = if c then current(n(x))
+ y = if c then n(x)
else d -> pre y;
tel
end
diff --git a/src/test/test.res.exp b/src/test/test.res.exp
index ad14bdd3..71417b0c 100644
--- a/src/test/test.res.exp
+++ b/src/test/test.res.exp
@@ -28,26 +28,9 @@ let
co = (((ci and x) or (x and y)) or (y and ci));
tel
-- end of node Int8::fulladd
-function Int8::incr(x:bool^8) returns (incr:bool^8);
-var
- co:bool;
-let
- (co, incr) = fillred<<node Int8::fulladd, const 8>>(true, x, zero);
-tel
--- end of node Int8::incr
-function Int8::add(x:bool^8; y:bool^8) returns (sum:bool^8);
-var
- co:bool;
-let
- (co, sum) = fillred<<node Int8::fulladd, const 8>>(false, x, y);
-tel
--- end of node Int8::add
-node mainPack::Nat(evt:bool; reset:bool) returns (nat:Int8::Int);
-let
- nat = if (true -> reset) then (Int8::zero) else ( if (evt) then
- (Int8::incr(pre(nat))) else (pre(nat)));
-tel
--- end of node mainPack::Nat
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/NONREG/Int.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/NONREG/PCOND.lus
@@ -1108,26 +1091,9 @@ extern node clock::all(
returns (
c:bool when b;
d:bool when c);
-node clock::clock(in:bool) returns (ok:bool);
-var
- v1:bool;
- v4:bool;
- v2:bool when v4;
- v3:bool when v1;
- v5:bool when v4;
- v6:bool when v5;
- v7:bool when v6;
-let
- v1 = clock::inOnIn(in, true when in);
- v2 = in when v4;
- v3 = clock::outOnIn(in, v1);
- (v4, v5) = clock::outOnOut(pre(v4), pre(v4));
- (v6, v7) = clock::all(v4, v5);
- ok = boolred<<const 3, const 3, const 7>>([v1, current (v2), current (v3),
- v4, current (v5), current (current (v6)), current (current (current
- (v7)))]);
-tel
--- end of node clock::clock
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/NONREG/clock.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/NONREG/cminus.lus
@@ -2958,17 +2924,9 @@ tel
====> ../lus2lic -vl 2 --compile-all-items should_work/Pascal/left.lus
Opening file /home/jahier/lus2lic/src/test/should_work/Pascal/left.lus
type left::truc = left::truc {a : bool^100; b : int};
-node left::toto(x:bool) returns (t:left::truc^3);
-let
- t[0].a[0..98 step 2][48..0 step -2] = true^25;
- t[0].a[0..98 step 2][1..49 step 2] = false^25;
- t[0].a[1..99 step 2][0] = true;
- t[0].a[1..99 step 2][1] = true;
- t[0].a[5..99 step 2] = false^48;
- t[0].b = 42;
- t[1..2] = truc{a=true^100;b=0}^2;
-tel
--- end of node left::toto
+
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/Pascal/left.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/Pascal/newpacks.lus
@@ -2993,26 +2951,8 @@ tel
-- end of node pint::fby1
type inter::selType = inter::selType {i : int; b : bool; r : real};
-node inter::preced(
- in:inter::selType)
-returns (
- out:inter::selType;
- out2:inter::selType);
-let
- out2 = selType{i=0;b=true;r=.0};
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
-tel
--- end of node inter::preced
-node mainPack::preced(in:inter::selType) returns (out:inter::selType);
-var
- out2:inter::selType;
-let
- (out, out2) = inter::preced(in);
-tel
--- end of node mainPack::preced
-const inter::n = -4;
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/Pascal/newpacks.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/Pascal/onlyroll.lus
@@ -3522,26 +3462,8 @@ tel
-- end of node pint::fby1
type inter::selType = inter::selType {i : int; b : bool; r : real};
-node inter::preced(
- in:inter::selType)
-returns (
- out:inter::selType;
- out2:inter::selType);
-let
- out2 = selType{i=0;b=true;r=.0};
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
-tel
--- end of node inter::preced
-node mainPack::preced(in:inter::selType) returns (out:inter::selType);
-var
- out2:inter::selType;
-let
- (out, out2) = inter::preced(in);
-tel
--- end of node mainPack::preced
-const inter::n = -4;
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/Pascal/p.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/Pascal/packs.lus
@@ -3574,28 +3496,8 @@ const mainPack::rose;
const mainPack::X = 8;
type inter::selType = inter::selType {i : int; b : bool; r : real};
-node inter::preced(
- in:inter::selType)
-returns (
- out:inter::selType;
- out2:inter::selType);
-let
- out2 = selType{i=0;b=true;r=0.0};
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
-tel
--- end of node inter::preced
-node mainPack::preced(in:inter::selType) returns (out:inter::selType);
-var
- out2:inter::selType;
-let
- (out, out2) = inter::preced(in);
-tel
--- end of node mainPack::preced
-type inter::toto = enum {inter::X, inter::Y};
-const inter::X;
-const inter::Y;
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/Pascal/packs.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/Pascal/pfs.lus
@@ -3607,11 +3509,9 @@ Opening file /home/jahier/lus2lic/src/test/should_work/Pascal/pfs.lus
====> ../lus2lic -vl 2 --compile-all-items should_work/Pascal/struct0.lus
Opening file /home/jahier/lus2lic/src/test/should_work/Pascal/struct0.lus
type struct0::Toto = struct0::Toto {x : int (1); y : int (2)};
-node struct0::bibi(dummy:int) returns (z:struct0::Toto);
-let
- z = Toto{x=3};
-tel
--- end of node struct0::bibi
+
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/Pascal/struct0.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/Pascal/t.lus
@@ -3660,7 +3560,7 @@ tel
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/call/bad_call02.lus
Opening file /home/jahier/lus2lic/src/test/should_work/call/bad_call02.lus
-node bad_call02::bad_call02(a:int; c:bool) returns (x:int);
+node bad_call02::bad_call02(a:int; c:bool) returns (x:int when c);
let
x = a when c;
tel
@@ -3786,13 +3686,24 @@ extern node clock::clock4(
returns (
clock4_x:bool;
clock4_y:bool when clock4_x);
+
+extern node clock::clock5(
+ x:bool;
+ y:bool when x;
+ z:bool when y)
+returns (
+ a:bool);
node clock::clock(a:bool; b:bool) returns (c:bool; d:bool when c);
var
z:bool;
+ z2:bool;
x:bool when z;
+ e:bool when a;
let
(z, x) = clock::clock3(z);
+ e = b when a;
(c, d) = clock::clock4(a, b when a);
+ z2 = clock::clock5(a, b when a, c when e);
tel
-- end of node clock::clock
@@ -3802,13 +3713,6 @@ extern node clock::clock2(
returns (
clock2_y:bool);
-extern node clock::clock5(
- x:bool;
- y:bool when x;
- z:bool when y)
-returns (
- a:bool);
-
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/Gyroscope2.lus
Opening file /home/jahier/lus2lic/src/test/should_work/demo/Gyroscope2.lus
@@ -3870,341 +3774,8 @@ let
tel
-- end of node Gyroscope2::TooFar
-node Gyroscope2::assumeEvaluateAxis(
- channels:Gyroscope2::Faulty_ChannelT^4;
- delta:real;
- god:real;
- delta_to_god:real)
-returns (
- assumeOK:bool);
-var
- NbToFar:int;
-let
- NbToFar = red<<node Gyroscope2::TooFar, const 4>>(0, channels, god^4,
- delta_to_god^4);
- assumeOK = (NbToFar <= 1);
-tel
--- end of node Gyroscope2::assumeEvaluateAxis
-
-node Gyroscope2::assumeChannel(
- previousOutChannel:Gyroscope2::Valid_ChannelT^4;
- nbInChannel:int;
- inChannel:Gyroscope2::Faulty_ChannelT;
- delta:real;
- god:real;
- delta_to_god:real)
-returns (
- assumeOK:bool);
-let
- assumeOK = true;
-tel
--- end of node Gyroscope2::assumeChannel
-
-node Gyroscope2::countValidChannels(
- channels:Gyroscope2::Valid_ChannelT^4)
-returns (
- nb:real);
-let
- nb = red<<node Gyroscope2::countFalse, const 4>>(0.0, channels);
-tel
--- end of node Gyroscope2::countValidChannels
-node Gyroscope2::sum(accu_in:real; elt_in:real) returns (accu_out:real);
-let
- accu_out = (accu_in + elt_in);
-tel
--- end of node Gyroscope2::sum
-
-node Gyroscope2::masking(
- channel:Gyroscope2::Valid_ChannelT)
-returns (
- out:real);
-let
- out = if (channel.local_failure) then (0.0) else (channel.local_value);
-tel
--- end of node Gyroscope2::masking
-
-node Gyroscope2::Voter(
- channels:Gyroscope2::Valid_ChannelT^4;
- god:real;
- delta_to_god:real)
-returns (
- vote:real);
-var
- globalSum:real;
- nbValid:real;
- mask:real^4;
-let
- nbValid = Gyroscope2::countValidChannels(channels);
- globalSum = red<<node Gyroscope2::sum, const 4>>(0.0, mask);
- vote = (globalSum / nbValid);
- mask = map<<node Gyroscope2::masking, const 4>>(channels);
-tel
--- end of node Gyroscope2::Voter
-
-node Gyroscope2::selectFailure(
- from:Gyroscope2::Valid_ChannelT)
-returns (
- failure:bool);
-let
- failure = from.local_failure;
-tel
--- end of node Gyroscope2::selectFailure
-
-node Gyroscope2::addOneChannelIter(
- acc_in:Gyroscope2::CFF_Eltstruct;
- elt_in:Gyroscope2::Valid_ChannelT)
-returns (
- acc_out:Gyroscope2::CFF_Eltstruct;
- elt_out:Gyroscope2::Valid_ChannelT);
-let
- acc_out = CFF_Eltstruct{indx=(acc_in.indx +
- 1);indx_toChange=acc_in.indx_toChange;value=acc_in.value};
- elt_out = if ((acc_in.indx = acc_in.indx_toChange)) then (acc_in.value)
- else (elt_in);
-tel
--- end of node Gyroscope2::addOneChannelIter
-
-node Gyroscope2::addOneChannel(
- indx_toChange:int;
- channeltToAdd:Gyroscope2::Valid_ChannelT;
- tabToFill:Gyroscope2::Valid_ChannelT^3)
-returns (
- tabToFillAfter:Gyroscope2::Valid_ChannelT^3);
-var
- acc_out:Gyroscope2::CFF_Eltstruct;
-let
- (acc_out, tabToFillAfter) = fillred<<node Gyroscope2::addOneChannelIter,
- const
- 3>>(CFF_Eltstruct{indx=0;indx_toChange=indx_toChange;value=channeltToAdd},
- tabToFill);
-tel
--- end of node Gyroscope2::addOneChannel
-
-node Gyroscope2::CFC_iter(
- structIn:Gyroscope2::CFF_struct;
- currentChannel:Gyroscope2::Valid_ChannelT)
-returns (
- structOut:Gyroscope2::CFF_struct);
-let
- structOut = CFF_struct{indx=(structIn.indx +
- 1);indx_toChange=structIn.indx_toChange;tabToFill= if
- ((structIn.indx_toChange = structIn.indx)) then (structIn.tabToFill) else
- (Gyroscope2::addOneChannel(structIn.indx, currentChannel,
- structIn.tabToFill))};
-tel
--- end of node Gyroscope2::CFC_iter
-
-node Gyroscope2::ComputeForeignChannels(
- currentChannelIndx:int;
- allChannels:Gyroscope2::Valid_ChannelT^4)
-returns (
- foreignChannels:Gyroscope2::Valid_ChannelT^3);
-var
- acc_out:Gyroscope2::CFF_struct;
- localtabToFill:Gyroscope2::Valid_ChannelT;
-let
- localtabToFill = Valid_ChannelT{local_failure=false;local_value=0.0};
- acc_out = red<<node Gyroscope2::CFC_iter, const
- 4>>(CFF_struct{indx=0;indx_toChange=currentChannelIndx;tabToFill=localtabToFill^3},
- allChannels);
- foreignChannels = acc_out.tabToFill;
-tel
--- end of node Gyroscope2::ComputeForeignChannels
-
-node Gyroscope2::compare_rolls(
- acc_in:Gyroscope2::Valid_ChannelT;
- channel:Gyroscope2::Valid_ChannelT)
-returns (
- acc_out:Gyroscope2::Valid_ChannelT;
- diff:bool);
-let
- acc_out = acc_in;
- diff = (Gyroscope2::abs((acc_in.local_value - channel.local_value)) >
- CROSS_CHANNEL_TOLERANCE);
-tel
--- end of node Gyroscope2::compare_rolls
-
-node Gyroscope2::values_nok(
- localChannel:Gyroscope2::Valid_ChannelT;
- foreign_Channels:Gyroscope2::Valid_ChannelT^3)
-returns (
- cross_failure:bool);
-var
- diff:bool^3;
- lc:Gyroscope2::Valid_ChannelT;
-let
- (lc, diff) = fillred<<node Gyroscope2::compare_rolls, const
- 3>>(localChannel, foreign_Channels);
- cross_failure = if (Gyroscope2::selectFailure(foreign_Channels[0])) then
- ( if (Gyroscope2::selectFailure(foreign_Channels[1])) then ( if
- (Gyroscope2::selectFailure(foreign_Channels[2])) then (false) else
- (diff[2])) else ( if (Gyroscope2::selectFailure(foreign_Channels[2])) then
- (diff[1]) else ((diff[1] and diff[2])))) else ( if
- (Gyroscope2::selectFailure(foreign_Channels[1])) then ( if
- (Gyroscope2::selectFailure(foreign_Channels[2])) then (diff[0]) else
- ((diff[0] and diff[2]))) else ( if
- (Gyroscope2::selectFailure(foreign_Channels[2])) then ((diff[0] and
- diff[1])) else (((diff[0] and diff[1]) and diff[2]))));
-tel
--- end of node Gyroscope2::values_nok
-
-node Gyroscope2::CrossFailDetect(
- currentChannel:int;
- localChannel:Gyroscope2::Valid_ChannelT;
- previousOutChannel:Gyroscope2::Valid_ChannelT^4)
-returns (
- crossFailure:bool);
-var
- foreign_Channels:Gyroscope2::Valid_ChannelT^3;
-let
- foreign_Channels = Gyroscope2::ComputeForeignChannels(currentChannel,
- previousOutChannel);
- crossFailure = Gyroscope2::values_nok(localChannel, foreign_Channels);
-tel
--- end of node Gyroscope2::CrossFailDetect
-
-node Gyroscope2::Channel(
- previousOutChannel:Gyroscope2::Valid_ChannelT^4;
- nbInChannel:int;
- inChannel:Gyroscope2::Faulty_ChannelT;
- delta:real;
- god:real;
- delta_to_god:real)
-returns (
- nextOutChannel:Gyroscope2::Valid_ChannelT^4;
- outChannel:Gyroscope2::Valid_ChannelT);
-var
- localChannel:Gyroscope2::Valid_ChannelT;
-let
- localChannel =
- Valid_ChannelT{local_failure=(Gyroscope2::abs((inChannel.valuea -
- inChannel.valueb)) > delta);local_value= if
- ((Gyroscope2::abs((inChannel.valuea - inChannel.valueb)) > delta)) then
- (0.0) else (((inChannel.valuea + inChannel.valueb) / 2.0))};
- outChannel = Valid_ChannelT{local_failure=(localChannel.local_failure or
- Gyroscope2::CrossFailDetect(nbInChannel, localChannel,
- previousOutChannel));local_value=localChannel.local_value};
- nextOutChannel = previousOutChannel;
-tel
--- end of node Gyroscope2::Channel
-
-node Gyroscope2::guaranteeChannel(
- previousOutChannel:Gyroscope2::Valid_ChannelT^4;
- nbInChannel:int;
- inChannel:Gyroscope2::Faulty_ChannelT;
- delta:real;
- god:real;
- delta_to_god:real;
- nextOutChannel:Gyroscope2::Faulty_ChannelT^4;
- outChannel:Gyroscope2::Valid_ChannelT)
-returns (
- guaranteeOK:bool);
-let
- guaranteeOK = (outChannel.local_failure or
- ((Gyroscope2::abs((inChannel.valuea - outChannel.local_value)) < delta) and
- (Gyroscope2::abs((inChannel.valueb - outChannel.local_value)) < delta)));
-tel
--- end of node Gyroscope2::guaranteeChannel
-
-node Gyroscope2::iteratedVoter(
- acc_in:bool;
- channel:Gyroscope2::Valid_ChannelT;
- god:real;
- delta_to_god:real;
- vote:real)
-returns (
- acc_out:bool);
-let
- acc_out = (acc_in and (channel.local_failure or (Gyroscope2::abs((vote -
- channel.local_value)) < delta_to_god)));
-tel
--- end of node Gyroscope2::iteratedVoter
-
-node Gyroscope2::assumeVoter(
- channels:Gyroscope2::Valid_ChannelT^4;
- god:real;
- delta_to_god:real)
-returns (
- assumeOK:bool);
-let
- assumeOK = true;
-tel
--- end of node Gyroscope2::assumeVoter
-
-node Gyroscope2::guaranteeEvaluateAxis(
- channels:Gyroscope2::Faulty_ChannelT^4;
- delta:real;
- god:real;
- delta_to_god:real;
- AxisValue:real)
-returns (
- guaranteeOK:bool);
-let
- guaranteeOK = (Gyroscope2::abs((AxisValue - god)) < delta_to_god);
-tel
--- end of node Gyroscope2::guaranteeEvaluateAxis
-
-node Gyroscope2::ValueIsSecure(
- secure_value:real;
- delta_to_god_value:real;
- god_value:real)
-returns (
- is_valid:bool);
-let
- is_valid = (Gyroscope2::abs((secure_value - god_value)) <
- delta_to_god_value);
-tel
--- end of node Gyroscope2::ValueIsSecure
-
-node Gyroscope2::EvaluateAxis(
- channels:Gyroscope2::Faulty_ChannelT^4;
- delta:real;
- god:real;
- delta_to_god:real)
-returns (
- AxisValue:real);
-var
- resChannels:Gyroscope2::Valid_ChannelT^4;
- dumbChannel:Gyroscope2::Valid_ChannelT^4;
- initChannels:Gyroscope2::Valid_ChannelT^4;
- fillredInit:Gyroscope2::Valid_ChannelT^4;
-let
- initChannels = Valid_ChannelT{local_failure=false;local_value=0.0}^4;
- (dumbChannel, resChannels) = fillred<<node Gyroscope2::Channel, const
- 4>>(fillredInit, [0, 1, 2, 3], channels, delta^4, god^4, delta_to_god^4);
- AxisValue = Gyroscope2::Voter(resChannels, god, delta_to_god);
- fillredInit = initChannels -> pre(resChannels);
-tel
--- end of node Gyroscope2::EvaluateAxis
-
-node Gyroscope2::Gyroscope2(
- axis:Gyroscope2::Faulty_ChannelT^4^3)
-returns (
- valid:bool);
-var
- secure_values:real^3;
-let
- secure_values = map<<node Gyroscope2::EvaluateAxis, const 3>>(axis,
- [DELTA_ROLL, DELTA_PITCH, DELTA_YAW], [GOD_ROLL, GOD_PITCH, GOD_YAW],
- [DELTA_TO_GOD_ROLL, DELTA_TO_GOD_PITCH, DELTA_TO_GOD_YAW]);
- valid = red<<node Gyroscope2::ValueIsSecureII, const 3>>(true,
- secure_values, [DELTA_TO_GOD_ROLL, DELTA_TO_GOD_PITCH, DELTA_TO_GOD_YAW],
- [GOD_ROLL, GOD_PITCH, GOD_YAW]);
-tel
--- end of node Gyroscope2::Gyroscope2
-
-node Gyroscope2::guaranteeVoter(
- channels:Gyroscope2::Valid_ChannelT^4;
- god:real;
- delta_to_god:real;
- vote:real)
-returns (
- guaranteeOK:bool);
-let
- guaranteeOK = red<<node Gyroscope2::iteratedVoter, const 4>>(true,
- channels, god^4, delta_to_god^4, vote^4);
-tel
--- end of node Gyroscope2::guaranteeVoter
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/Gyroscope2.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/alias.lus
@@ -4238,31 +3809,24 @@ let
o = Lustre::not(i);
tel
-- end of node alias::aliasPredefNot
-node alias::alias(a:bool) returns (b:bool; c:int);
-let
- b = alias::aliasPredefNot(a);
- c = alias::aliasGivenNode(0, map<<node Lustre::+, const 3>>(0^3, SIZE^3));
-tel
--- end of node alias::alias
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/alias.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/bred.lus
Opening file /home/jahier/lus2lic/src/test/should_work/demo/bred.lus
-node bred::bred(a:bool^2) returns (x:bool);
-let
- x = boolred<<const 0, const 1, const 2>>(a);
-tel
--- end of node bred::bred
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/bred.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/bred_lv4.lus
Opening file /home/jahier/lus2lic/src/test/should_work/demo/bred_lv4.lus
type bred_lv4::T1_ARRAY = bool^2;
-node bred_lv4::bred(i_a:bool^2) returns (o_x:bool);
-let
- o_x = boolred<<const 0, const 1, const 2>>(i_a);
-tel
--- end of node bred_lv4::bred
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/bred_lv4.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/clock.lus
@@ -4496,30 +4060,9 @@ let
elt = acc_in;
tel
-- end of node filliter::copie
-node filliter::incr_acc(acc_in:int) returns (acc_out:int; res:int);
-let
- res = acc_in;
- acc_out = (res + 1);
-tel
--- end of node filliter::incr_acc
-node filliter::filliter(
- c:bool;
- i1:int when c;
- i2:int when c)
-returns (
- s1:int^3 when c;
- s2:int^3 when c);
-var
- x:int^4 when c;
- bid1:int when c;
- bid2:int when c;
-let
- s1 = x[0..2];
- (bid1, x) = fill<<node filliter::copie, const 4>>(i1);
- (bid2, s2) = fill<<node filliter::incr_acc, const 3>>(i2);
-tel
--- end of node filliter::filliter
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/filliter.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/filter.lus
@@ -4635,21 +4178,8 @@ let
tel
-- end of node map_red_iter::traite_genCore_itere
-node map_red_iter::map_red_iter(
- indice_gen:int;
- InfoGenIndiv:map_red_iter::T_InfoGenIndiv;
- InfoGenGlob:map_red_iter::T_InfoGenGlob;
- TabEtatCharge:int^20;
- TabComVal:bool^20)
-returns (
- TabComChg:int^20);
-var
- bidon:int;
-let
- (bidon, TabComChg) = fillred<<node map_red_iter::traite_genCore_itere,
- const 20>>(indice_gen, TabComVal, InfoGenGlob.chg2gen);
-tel
--- end of node map_red_iter::map_red_iter
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/map_red_iter.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/mapdeRed.lus
@@ -4664,19 +4194,8 @@ let
tel
-- end of node mapdeRed::incr
-node mapdeRed::mapdeRed(
- init:int^2;
- init2:int)
-returns (
- r:int^2;
- T:int^2^3;
- bid:int);
-let
- (bid, T) = fill<<node Lustre::fill<<node mapdeRed::incr, const 2>>, const
- 3>>(init2);
- r = red<<node Lustre::map<<node Lustre::+, const 2>>, const 3>>(init, T);
-tel
--- end of node mapdeRed::mapdeRed
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/mapdeRed.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/mapiter.lus
@@ -4686,12 +4205,9 @@ let
b = (a + 1);
tel
-- end of node mapiter::incr_tab
-node mapiter::mapiter(i1:int^7^3) returns (s1:int^7^3);
-let
- s1 = map<<node Lustre::map<<node mapiter::incr_tab, const 7>>, const
- 3>>(i1);
-tel
--- end of node mapiter::mapiter
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/mapiter.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/mappredef.lus
@@ -4700,34 +4216,15 @@ const mappredef::N = 3;
type mappredef::tab_int = int^3;
type mappredef::tab_bool = bool^3;
-node mappredef::mappredef(
- x:bool^3;
- a:int^3;
- b:int^3)
-returns (
- c:int^3;
- d:int^3);
-var
- z:int;
-let
- z = if (x[0]) then (a[0]) else (b[0]);
- c = map<<node Lustre::if, const 3>>(x, a, b);
- d = map<<node Lustre::-, const 3>>(b);
-tel
--- end of node mappredef::mappredef
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/mappredef.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/plus.lus
Opening file /home/jahier/lus2lic/src/test/should_work/demo/plus.lus
-node plus::plus(a:int; b:int) returns (c:int; d:int; e:int; f:int);
-let
- c = (a + b);
- d = (a + b);
- e = if (boolred<<const 0, const 1, const 2>>(true^2)) then (a) else (b);
- f = if (nor((c < b), (c <= b))) then (a) else ((b + if (boolred<<const
- 0, const 0, const 2>>([(c < b), (c <= b)])) then (a) else (b)));
-tel
--- end of node plus::plus
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/plus.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/pre_x.lus
@@ -4746,11 +4243,9 @@ let
b = if ((init > a)) then (init) else (a);
tel
-- end of node rediter::max
-node rediter::rediter(a:int^5^3) returns (b:int);
-let
- b = red<<node Lustre::red<<node rediter::max, const 5>>, const 3>>(0, a);
-tel
--- end of node rediter::rediter
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/rediter.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/redoptest.lus
@@ -4760,11 +4255,9 @@ let
b = if ((init > a)) then (init) else (a);
tel
-- end of node redoptest::max
-node redoptest::redoptest(a:int^5^3) returns (b:int);
-let
- b = red<<node Lustre::red<<node Lustre::+, const 5>>, const 3>>(0, a);
-tel
--- end of node redoptest::redoptest
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/demo/redoptest.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/sample_time_change.lus
@@ -4902,47 +4395,9 @@ let
elt = accu_in;
tel
-- end of node iter::filled
-node iter::mapped(elt_in:int) returns (elt_out:int);
-let
- elt_out = (elt_in + 1);
-tel
--- end of node iter::mapped
-
-node iter::garcia(
- accu_in:int;
- elt_in:int)
-returns (
- accu_out:int;
- elt_out:int);
-let
- accu_out = (accu_in + 1);
- elt_out = (elt_in + accu_out);
-tel
--- end of node iter::garcia
-node iter::iter(
- init:int)
-returns (
- Tab_out:int^5;
- Red_plus:int;
- zorroTab:int^5;
- zorroAcc:int);
-var
- T_inter:int^5;
- bidon:int;
-let
- (bidon, T_inter) = fill<<node iter::filled, const 5>>(init);
- Tab_out = map<<node iter::mapped, const 5>>(T_inter);
- Red_plus = red<<node Lustre::+, const 5>>(-(100), Tab_out);
- (zorroAcc, zorroTab) = fillred<<node iter::garcia, const 5>>(0, [0, 0, 0,
- 0, 0]);
-tel
--- end of node iter::iter
-node iter::plus(accu_in:int; elt_in:int) returns (accu_out:int);
-let
- accu_out = (accu_in + elt_in);
-tel
--- end of node iter::plus
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/fab_test/iter.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/fab_test/iterate.lus
@@ -4960,70 +4415,8 @@ let
tel
-- end of node iterate::mapped
-node iterate::redduced(
- accu_in:int;
- elt_in1:int;
- elt_in2:int)
-returns (
- accu_out:int);
-let
- accu_out = ((accu_in + elt_in1) + elt_in2);
-tel
--- end of node iterate::redduced
-
-node iterate::filled(
- accu_in:int)
-returns (
- accu_out:int;
- elt_out1:int;
- elt_out2:int);
-let
- accu_out = (accu_in + 1);
- elt_out1 = accu_in;
- elt_out2 = (accu_in * 2);
-tel
--- end of node iterate::filled
-
-node iterate::fill_redduced(
- accu_in:int;
- elt_in1:int;
- elt_in2:int)
-returns (
- accu_out:int;
- elt_out1:int;
- elt_out2:int;
- elt_out3:int);
-let
- accu_out = (accu_in + 1);
- elt_out1 = elt_in1;
- elt_out2 = elt_in2;
- elt_out3 = (elt_in1 + elt_in2);
-tel
--- end of node iterate::fill_redduced
-
-node iterate::iterate(
- IN1:int^10;
- IN2:int^10)
-returns (
- OUT:int^10;
- out_map1:int^10;
- out_map2:int^10;
- out_red1:int;
- out_fill1:int^10;
- out_fill2:int^10;
- out_fillred1:int;
- out_fillred2:int^10;
- out_fillred3:int^10);
-var
- bidon:int;
-let
- (out_map1, out_map2) = map<<node iterate::mapped, const 10>>(IN1, IN2);
- out_red1 = red<<node iterate::redduced, const 10>>(0, IN1, IN2);
- (bidon, out_fill1, out_fill2) = fill<<node iterate::filled, const 10>>(0);
- (out_fillred1, out_fillred2, out_fillred3, OUT) = fillred<<node
- iterate::fill_redduced, const 10>>(0, IN1, IN2);
-tel
--- end of node iterate::iterate
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/fab_test/iterate.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/fab_test/lecteur.lus
@@ -5268,54 +4661,9 @@ type morel4::tube = morel4::tube {in : int; out : int};
type morel4::toto = morel4::toto {titi : morel4::tube; tutu : bool};
type morel4::arrayb = bool^3;
type morel4::arrayi = int^2^3;
-node morel4::mcmorel(i:int) returns (t:int^2);
-var
- yo:morel4::toto;
-let
- yo.titi = tube{in=i;out=(i + 1)};
- yo.tutu = true;
- t = [yo.titi.in, yo.titi.out] -> [(pre(t[0]) + 1), pre(t[1])];
-tel
--- end of node morel4::mcmorel
-node morel4::tab(
- b:bool;
- i:int)
-returns (
- b1:bool;
- b2:bool;
- b3:bool;
- i1:int;
- i2:int;
- i3:int);
-var
- tabb:bool^3;
- tabi:int^2^3;
-let
- (b1, b2, b3) = (tabb[0], tabb[1], tabb[2]);
- (i1, i2, i3) = ((tabi[0][0] + tabi[0][1]), (tabi[1][0] + tabi[1][1]),
- (tabi[2][0] + tabi[2][1]));
- tabb[0] = b;
- tabb[1..2] = [true, false];
- tabi[2] = morel4::mcmorel(i);
- tabi[0..1] = [[10, 100], [1000, 10000]];
-tel
--- end of node morel4::tab
-
-node morel4::morel4(
- b:bool;
- i:int)
-returns (
- b1:bool;
- b2:bool;
- b3:bool;
- i1:int;
- i2:int;
- i3:int);
-let
- (b1, b2, b3, i1, i2, i3) = morel4::tab(b, i);
-tel
--- end of node morel4::morel4
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/fab_test/morel4.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/fab_test/morel5.lus
@@ -5358,16 +4706,9 @@ let
(b1, b2, b3, i1, i2, i3) = morel5::tab(t, b, i);
tel
-- end of node morel5::morel5
-node morel5::mcmorel(i:int) returns (t:int^2; u:int^2^2);
-var
- yo:morel5::toto;
-let
- yo.titi = tube{in=i;out=(i + 1)};
- yo.tutu = true;
- t = [yo.titi.in, yo.titi.out] -> [(pre(t[0]) + 1), pre(t[1])];
- u = [[10, 100], [1000, 10000]];
-tel
--- end of node morel5::mcmorel
+
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/fab_test/morel5.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/fab_test/noAlarm.lus
@@ -6506,19 +5847,8 @@ let
tel
-- end of node FillFollowedByRed::filled
-node FillFollowedByRed::FillFollowedByRed(
- initFill:real)
-returns (
- ok:bool);
-var
- TabOutFill:real^10;
- bidon:real;
-let
- (bidon, TabOutFill) = fill<<node FillFollowedByRed::filled, const
- 10>>(initFill);
- ok = red<<node FillFollowedByRed::reduced, const 10>>(true, TabOutFill);
-tel
--- end of node FillFollowedByRed::FillFollowedByRed
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/FillFollowedByRed.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/Gyroscope.lus
@@ -6579,263 +5909,8 @@ let
tel
-- end of node Gyroscope::TooFar
-node Gyroscope::assumeEvaluateAxis(
- channels:Gyroscope::Faulty_ChannelT^4;
- delta:real;
- god:real;
- delta_to_god:real)
-returns (
- assumeOK:bool);
-var
- NbToFar:int;
-let
- NbToFar = red<<node Gyroscope::TooFar, const 4>>(0, channels, god^4,
- delta_to_god^4);
- assumeOK = (NbToFar <= 1);
-tel
--- end of node Gyroscope::assumeEvaluateAxis
-
-node Gyroscope::assumeSum(
- accu_in:real;
- elt_in:real)
-returns (
- assumeOK:bool);
-var
- varBidon:real;
-let
- varBidon = 1.0;
- assumeOK = (varBidon < elt_in);
-tel
--- end of node Gyroscope::assumeSum
-
-node Gyroscope::assumeChannel(
- inChannel:Gyroscope::Faulty_ChannelT;
- delta:real;
- god:real;
- delta_to_god:real)
-returns (
- assumeOK:bool);
-let
- assumeOK = true;
-tel
--- end of node Gyroscope::assumeChannel
-node Gyroscope::min_int(n1:int; n2:int) returns (n:int);
-let
- n = if ((n1 > n2)) then (n2) else (n1);
-tel
--- end of node Gyroscope::min_int
-node Gyroscope::Maintain(n:int; val:bool) returns (m:bool);
-var
- cpt:int;
-let
- cpt = if (val) then (1) else (0) -> if (val) then (Gyroscope::min_int(n,
- (pre(cpt) + 1))) else (0);
- m = (cpt >= n);
-tel
--- end of node Gyroscope::Maintain
-
-node Gyroscope::Channel(
- inChannel:Gyroscope::Faulty_ChannelT;
- delta:real;
- god:real;
- delta_to_god:real)
-returns (
- outChannel:Gyroscope::Valid_ChannelT);
-var
- maintain:bool;
-let
- maintain = Gyroscope::Maintain(TIME, (Gyroscope::abs((inChannel.valuea -
- inChannel.valueb)) > delta));
- outChannel = Valid_ChannelT{local_failure=maintain;local_value= if
- (maintain) then (0.0) else (((inChannel.valuea + inChannel.valueb) /
- 2.0))};
-tel
--- end of node Gyroscope::Channel
-
-node Gyroscope::countValidChannels(
- channels:Gyroscope::Valid_ChannelT^4)
-returns (
- nb:real);
-let
- nb = red<<node Gyroscope::countFalse, const 4>>(0.0, channels);
-tel
--- end of node Gyroscope::countValidChannels
-node Gyroscope::sum(accu_in:real; elt_in:real) returns (accu_out:real);
-let
- accu_out = (accu_in + elt_in);
-tel
--- end of node Gyroscope::sum
-
-node Gyroscope::masking(
- channel:Gyroscope::Valid_ChannelT)
-returns (
- out:real);
-let
- out = if (channel.local_failure) then (0.0) else (channel.local_value);
-tel
--- end of node Gyroscope::masking
-
-node Gyroscope::Voter(
- channels:Gyroscope::Valid_ChannelT^4;
- god:real;
- delta_to_god:real)
-returns (
- vote:real);
-var
- globalSum:real;
- nbValid:real;
- mask:real^4;
-let
- nbValid = Gyroscope::countValidChannels(channels);
- globalSum = red<<node Gyroscope::sum, const 4>>(0.0, mask);
- vote = (globalSum / nbValid);
- mask = map<<node Gyroscope::masking, const 4>>(channels);
-tel
--- end of node Gyroscope::Voter
-
-node Gyroscope::Voter2(
- channels:Gyroscope::Valid_ChannelT^4;
- god:real;
- delta_to_god:real)
-returns (
- vote:real);
-var
- globalSum:real;
- nbValid:real;
- mask:real^4;
-let
- nbValid = 0.0;
- globalSum = 0.0;
- vote = 0.0;
- mask = map<<node Gyroscope::masking, const 4>>(channels);
-tel
--- end of node Gyroscope::Voter2
-
-node Gyroscope::EvaluateAxis(
- channels:Gyroscope::Faulty_ChannelT^4;
- delta:real;
- god:real;
- delta_to_god:real)
-returns (
- AxisValue:real);
-var
- resChannels:Gyroscope::Valid_ChannelT^4;
- AxisValue2:real;
-let
- resChannels = map<<node Gyroscope::Channel, const 4>>(channels, delta^4,
- god^4, delta_to_god^4);
- AxisValue = Gyroscope::Voter(resChannels, god, delta_to_god);
- AxisValue2 = Gyroscope::Voter2(resChannels, god, delta_to_god);
-tel
--- end of node Gyroscope::EvaluateAxis
-
-node Gyroscope::Gyroscope(
- axis:Gyroscope::Faulty_ChannelT^4^3)
-returns (
- valid:bool);
-var
- secure_values:real^3;
-let
- secure_values = map<<node Gyroscope::EvaluateAxis, const 3>>(axis,
- [DELTA_ROLL, DELTA_PITCH, DELTA_YAW], [GOD_ROLL, GOD_PITCH, GOD_YAW],
- [DELTA_TO_GOD_ROLL, DELTA_TO_GOD_PITCH, DELTA_TO_GOD_YAW]);
- valid = red<<node Gyroscope::ValueIsSecureII, const 3>>(true,
- secure_values, [DELTA_TO_GOD_ROLL, DELTA_TO_GOD_PITCH, DELTA_TO_GOD_YAW],
- [GOD_ROLL, GOD_PITCH, GOD_YAW]);
-tel
--- end of node Gyroscope::Gyroscope
-
-node Gyroscope::guaranteeChannel(
- inChannel:Gyroscope::Faulty_ChannelT;
- delta:real;
- god:real;
- delta_to_god:real;
- outChannel:Gyroscope::Valid_ChannelT)
-returns (
- guaranteeOK:bool);
-let
- guaranteeOK = (outChannel.local_failure or
- ((Gyroscope::abs((inChannel.valuea - outChannel.local_value)) < delta) and
- (Gyroscope::abs((inChannel.valueb - outChannel.local_value)) < delta)));
-tel
--- end of node Gyroscope::guaranteeChannel
-
-node Gyroscope::iteratedVoter(
- acc_in:bool;
- channel:Gyroscope::Valid_ChannelT;
- god:real;
- delta_to_god:real;
- vote:real)
-returns (
- acc_out:bool);
-let
- acc_out = (acc_in and (channel.local_failure or (Gyroscope::abs((vote -
- channel.local_value)) < delta_to_god)));
-tel
--- end of node Gyroscope::iteratedVoter
-
-node Gyroscope::assumeVoter(
- channels:Gyroscope::Valid_ChannelT^4;
- god:real;
- delta_to_god:real)
-returns (
- assumeOK:bool);
-let
- assumeOK = true;
-tel
--- end of node Gyroscope::assumeVoter
-
-node Gyroscope::guaranteeEvaluateAxis(
- channels:Gyroscope::Faulty_ChannelT^4;
- delta:real;
- god:real;
- delta_to_god:real;
- AxisValue:real)
-returns (
- guaranteeOK:bool);
-let
- guaranteeOK = (Gyroscope::abs((AxisValue - god)) < delta_to_god);
-tel
--- end of node Gyroscope::guaranteeEvaluateAxis
-
-node Gyroscope::ValueIsSecure(
- secure_value:real;
- delta_to_god_value:real;
- god_value:real)
-returns (
- is_valid:bool);
-let
- is_valid = (Gyroscope::abs((secure_value - god_value)) <
- delta_to_god_value);
-tel
--- end of node Gyroscope::ValueIsSecure
-
-node Gyroscope::guaranteeSum(
- accu_in:real;
- elt_in:real;
- accu_out:real)
-returns (
- guaranteeOK:bool);
-var
- otherVarBidon:real;
-let
- otherVarBidon = 1.0;
- guaranteeOK = ((elt_in + otherVarBidon) < accu_out);
-tel
--- end of node Gyroscope::guaranteeSum
-
-node Gyroscope::guaranteeVoter(
- channels:Gyroscope::Valid_ChannelT^4;
- god:real;
- delta_to_god:real;
- vote:real)
-returns (
- guaranteeOK:bool);
-let
- guaranteeOK = red<<node Gyroscope::iteratedVoter, const 4>>(true,
- channels, god^4, delta_to_god^4, vote^4);
-tel
--- end of node Gyroscope::guaranteeVoter
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/Gyroscope.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/ProduitBool/produitBool.lus
@@ -6847,110 +5922,8 @@ type produitBool::iteratedStruct = produitBool::iteratedStruct {currentRank : in
type produitBool::Tacc_inShift2 = produitBool::Tacc_inShift2 {multiplieur : bool^10; rank : int; actual_rank : int};
type produitBool::Tacc_inShift = produitBool::Tacc_inShift {acc_in_PLC : produitBool::Tacc_in; actual_rank : int};
-node produitBool::iterated_isElementOf_(
- acc_in:produitBool::T_isElementOf_;
- elt_in:bool)
-returns (
- acc_out:produitBool::T_isElementOf_);
-let
- acc_out =
- T_isElementOf_{eltToSearch=acc_in.eltToSearch;iselementof=(acc_in.iselementof
- or (acc_in.eltToSearch = elt_in))};
-tel
--- end of node produitBool::iterated_isElementOf_
-
-node produitBool::_isElementOf_(
- e:bool;
- t:bool^10)
-returns (
- iselementof:bool);
-var
- acc_out:produitBool::T_isElementOf_;
-let
- acc_out = red<<node produitBool::iterated_isElementOf_, const
- 10>>(T_isElementOf_{eltToSearch=e;iselementof=false}, t);
- iselementof = acc_out.iselementof;
-tel
--- end of node produitBool::_isElementOf_
-
-node produitBool::selectOneStage(
- acc_in:produitBool::iteratedStruct;
- currentElt:bool)
-returns (
- acc_out:produitBool::iteratedStruct);
-let
- acc_out = iteratedStruct{currentRank=(acc_in.currentRank +
- 1);rankToSelect=acc_in.rankToSelect;elementSelected= if
- ((acc_in.currentRank = acc_in.rankToSelect)) then (currentElt) else
- (acc_in.elementSelected)};
-tel
--- end of node produitBool::selectOneStage
-
-node produitBool::selectElementOfRank_inArray_(
- rankToSelect:int;
- array:bool^10)
-returns (
- elementSelected:bool);
-var
- iterationResult:produitBool::iteratedStruct;
-let
- iterationResult = red<<node produitBool::selectOneStage, const
- 10>>(iteratedStruct{currentRank=0;rankToSelect=rankToSelect;elementSelected=array[0]},
- array);
- elementSelected = iterationResult.elementSelected;
-tel
--- end of node produitBool::selectElementOfRank_inArray_
-
-node produitBool::shiftFill(
- acc_in:produitBool::Tacc_inShift2)
-returns (
- acc_out:produitBool::Tacc_inShift2;
- elt_out:bool);
-let
- acc_out =
- Tacc_inShift2{multiplieur=acc_in.multiplieur;rank=acc_in.rank;actual_rank=(acc_in.actual_rank
- + 1)};
- elt_out = if (((acc_in.actual_rank >= acc_in.rank) and
- (acc_in.actual_rank < (acc_in.rank + size)))) then
- (produitBool::selectElementOfRank_inArray_((acc_in.actual_rank -
- acc_in.rank), acc_in.multiplieur)) else (false);
-tel
--- end of node produitBool::shiftFill
-
-node produitBool::shift(
- acc_in:produitBool::Tacc_in)
-returns (
- ligne:bool^20);
-var
- bidon:produitBool::Tacc_inShift2;
-let
- (bidon, ligne) = fill<<node produitBool::shiftFill, const
- 20>>(Tacc_inShift2{multiplieur=acc_in.multiplieur;rank=acc_in.rank;actual_rank=0});
-tel
--- end of node produitBool::shift
-
-node produitBool::produitBool(
- multiplicande:bool^10;
- multiplieur:bool^10)
-returns (
- matrice:bool^20^10);
-let
- matrice = true^20^10;
-tel
--- end of node produitBool::produitBool
-
-node produitBool::PLC(
- acc_in:produitBool::Tacc_in;
- multiplicande:bool)
-returns (
- acc_out:produitBool::Tacc_in;
- ligne:bool^20);
-let
- ligne = if ((multiplicande = false)) then (multiplicande^20) else
- (produitBool::shift(acc_in));
- acc_out = acc_in;
-tel
--- end of node produitBool::PLC
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/lionel/ProduitBool/produitBool.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/ProduitBool/shiftFill_ludic.lus
@@ -6968,49 +5941,8 @@ type shiftFill_ludic::T3_STRUCT = shiftFill_ludic::T3_STRUCT {currentRank : int;
type shiftFill_ludic::t_iteratedStruct = shiftFill_ludic::T3_STRUCT {currentRank : int; rankToSelect : int; elementSelected : bool};
const shiftFill_ludic::c_size = 10;
-node shiftFill_ludic::n_selectOneStage(
- i_acc_in:shiftFill_ludic::T3_STRUCT;
- i_currentElt:bool)
-returns (
- o_acc_out:shiftFill_ludic::T3_STRUCT);
-let
- o_acc_out = T3_STRUCT{currentRank=(i_acc_in.currentRank +
- 1);rankToSelect=i_acc_in.rankToSelect;elementSelected= if
- ((i_acc_in.currentRank = i_acc_in.rankToSelect)) then (i_currentElt) else
- (i_acc_in.elementSelected)};
-tel
--- end of node shiftFill_ludic::n_selectOneStage
-
-node shiftFill_ludic::n_selectElementOfRank_inArray_(
- i_rankToSelect:int;
- i_array:bool^10)
-returns (
- o_elementSelected:bool);
-var
- v_iterationResult:shiftFill_ludic::T3_STRUCT;
-let
- v_iterationResult = red<<node shiftFill_ludic::n_selectOneStage, const
- 10>>(T3_STRUCT{currentRank=0;rankToSelect=i_rankToSelect;elementSelected=i_array[0]},
- i_array);
- o_elementSelected = v_iterationResult.elementSelected;
-tel
--- end of node shiftFill_ludic::n_selectElementOfRank_inArray_
-
-node shiftFill_ludic::n_shiftFill(
- i_acc_in:shiftFill_ludic::T2_STRUCT)
-returns (
- o_acc_out:shiftFill_ludic::T2_STRUCT;
- o_elt_out:bool);
-let
- o_acc_out =
- T2_STRUCT{multiplieur=i_acc_in.multiplieur;rank=i_acc_in.rank;actual_rank=(i_acc_in.actual_rank
- + 1)};
- o_elt_out = if (((i_acc_in.actual_rank >= i_acc_in.rank) and
- (i_acc_in.actual_rank < (i_acc_in.rank + c_size)))) then
- (shiftFill_ludic::n_selectElementOfRank_inArray_(i_acc_in.actual_rank,
- i_acc_in.multiplieur)) else (false);
-tel
--- end of node shiftFill_ludic::n_shiftFill
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/lionel/ProduitBool/shiftFill_ludic.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/ProduitBool/shift_ludic.lus
@@ -7029,61 +5961,8 @@ type shift_ludic::t_Tacc_inShift2 = shift_ludic::T2_STRUCT {multiplieur : bool^1
type shift_ludic::t_iteratedStruct = shift_ludic::T4_STRUCT {currentRank : int; rankToSelect : int; elementSelected : bool};
const shift_ludic::c_size = 10;
-node shift_ludic::n_selectOneStage(
- i_acc_in:shift_ludic::T4_STRUCT;
- i_currentElt:bool)
-returns (
- o_acc_out:shift_ludic::T4_STRUCT);
-let
- o_acc_out = T4_STRUCT{currentRank=(i_acc_in.currentRank +
- 1);rankToSelect=i_acc_in.rankToSelect;elementSelected= if
- ((i_acc_in.currentRank = i_acc_in.rankToSelect)) then (i_currentElt) else
- (i_acc_in.elementSelected)};
-tel
--- end of node shift_ludic::n_selectOneStage
-
-node shift_ludic::n_selectElementOfRank_inArray_(
- i_rankToSelect:int;
- i_array:bool^10)
-returns (
- o_elementSelected:bool);
-var
- v_iterationResult:shift_ludic::T4_STRUCT;
-let
- v_iterationResult = red<<node shift_ludic::n_selectOneStage, const
- 10>>(T4_STRUCT{currentRank=0;rankToSelect=i_rankToSelect;elementSelected=i_array[0]},
- i_array);
- o_elementSelected = v_iterationResult.elementSelected;
-tel
--- end of node shift_ludic::n_selectElementOfRank_inArray_
-
-node shift_ludic::n_shiftFill(
- i_acc_in:shift_ludic::T2_STRUCT)
-returns (
- o_acc_out:shift_ludic::T2_STRUCT;
- o_elt_out:bool);
-let
- o_acc_out =
- T2_STRUCT{multiplieur=i_acc_in.multiplieur;rank=i_acc_in.rank;actual_rank=(i_acc_in.actual_rank
- + 1)};
- o_elt_out = if (((i_acc_in.actual_rank >= i_acc_in.rank) and
- (i_acc_in.actual_rank < (i_acc_in.rank + c_size)))) then
- (shift_ludic::n_selectElementOfRank_inArray_(i_acc_in.actual_rank,
- i_acc_in.multiplieur)) else (false);
-tel
--- end of node shift_ludic::n_shiftFill
-
-node shift_ludic::n_shift(
- i_acc_in:shift_ludic::T5_STRUCT)
-returns (
- o_ligne:bool^20);
-var
- v_bidon:shift_ludic::T2_STRUCT;
-let
- (v_bidon, o_ligne) = fill<<node shift_ludic::n_shiftFill, const
- 20>>(T2_STRUCT{multiplieur=i_acc_in.multiplieur;rank=i_acc_in.rank;actual_rank=0});
-tel
--- end of node shift_ludic::n_shift
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/lionel/ProduitBool/shift_ludic.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/arrays.lus
@@ -7101,77 +5980,9 @@ let
val = accin;
tel
-- end of node arrays::incr
-node arrays::big_sum(x:int^4^3^2) returns (s:int);
-let
- s = red<<node Lustre::red<<node Lustre::red<<node Lustre::+, const 4>>,
- const 3>>, const 2>>(0, x);
-tel
--- end of node arrays::big_sum
-node arrays::big_or(x:bool^4^3^2) returns (s:bool);
-let
- s = red<<node Lustre::red<<node Lustre::red<<node Lustre::or, const 4>>,
- const 3>>, const 2>>(false, x);
-tel
--- end of node arrays::big_or
-node arrays::big_incr(init:int) returns (x:int^4^3^2);
-var
- accout:int;
-let
- (accout, x) = fill<<node Lustre::fill<<node Lustre::fill<<node
- arrays::incr, const 4>>, const 3>>, const 2>>(init);
-tel
--- end of node arrays::big_incr
-node arrays::full_adder(
- ci:bool;
- x:bool;
- y:bool)
-returns (
- co:bool;
- s:bool);
-let
- s = ((ci xor x) xor y);
- co = if (ci) then ((x or y)) else ((x and y));
-tel
--- end of node arrays::full_adder
-node arrays::add_long(x:bool^4^3^2; y:bool^4^3^2) returns (s:bool^4^3^2);
-var
- co:bool;
-let
- (co, s) = fillred<<node Lustre::fillred<<node Lustre::fillred<<node
- arrays::full_adder, const 4>>, const 3>>, const 2>>(false, x, y);
-tel
--- end of node arrays::add_long
-node arrays::big_xor(x:bool^4^3^2) returns (s:bool);
-let
- s = red<<node Lustre::red<<node Lustre::red<<node Lustre::xor, const 4>>,
- const 3>>, const 2>>(false, x);
-tel
--- end of node arrays::big_xor
-
-node arrays::arrays(
- init_incr:int;
- init_long:bool^4^3^2)
-returns (
- ok:bool;
- red_res:int;
- fillred_res:bool^4^3^2);
-var
- fill_res:int^4^3^2;
-let
- red_res = arrays::big_sum(fill_res);
- fill_res = arrays::big_incr(init_incr);
- fillred_res = init_long -> arrays::add_long(init_long, pre(fillred_res));
- ok = false -> arrays::big_xor(fillred_res);
-tel
--- end of node arrays::arrays
-node arrays::add_byte(x:bool^4; y:bool^4) returns (s:bool^4);
-var
- co:bool;
-let
- (co, s) = fillred<<node arrays::full_adder, const 4>>(false, x, y);
-tel
--- end of node arrays::add_byte
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/arrays.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/calculs_max.lus
@@ -7182,46 +5993,8 @@ type calculs_max::int_arrays = int^10;
type calculs_max::struct_fill_bool = calculs_max::struct_fill_bool {imax1 : int; imax2 : int; icourant : int};
type calculs_max::struct_max = calculs_max::struct_max {max1 : int; max2 : int; imax1 : int; imax2 : int; icourant : int};
-node calculs_max::max(
- strin:calculs_max::struct_max;
- ecourant:int)
-returns (
- strout:calculs_max::struct_max);
-let
- strout = if ((ecourant <= strin.max2)) then
- (struct_max{max1=strin.max1;max2=strin.max2;imax1=strin.imax1;imax2=strin.imax2;icourant=(strin.icourant
- + 1)}) else ( if (((ecourant > strin.max2) and (ecourant <= strin.max1)))
- then
- (struct_max{max1=strin.max1;max2=ecourant;imax1=strin.imax1;imax2=strin.icourant;icourant=(strin.icourant
- + 1)}) else
- (struct_max{max1=ecourant;max2=strin.max1;imax1=strin.icourant;imax2=strin.imax1;icourant=(strin.icourant
- + 1)}));
-tel
--- end of node calculs_max::max
-
-node calculs_max::fill_bool(
- s_in:calculs_max::struct_fill_bool)
-returns (
- s_out:calculs_max::struct_fill_bool;
- elt:bool);
-let
- s_out =
- struct_fill_bool{imax1=s_in.imax1;imax2=s_in.imax2;icourant=(s_in.icourant
- + 1)};
- elt = ((s_in.icourant = s_in.imax1) or (s_in.icourant = s_in.imax2));
-tel
--- end of node calculs_max::fill_bool
-node calculs_max::calculs_max(A:int^10) returns (res:bool^10);
-var
- local_struct:calculs_max::struct_max;
- tmp:calculs_max::struct_fill_bool;
-let
- local_struct = red<<node calculs_max::max, const
- 10>>(struct_max{max1=0;max2=0;imax1=-(1);imax2=-(1);icourant=0}, A);
- (tmp, res) = fill<<node calculs_max::fill_bool, const
- 10>>(struct_fill_bool{imax1=local_struct.imax1;imax2=local_struct.imax2;icourant=0});
-tel
--- end of node calculs_max::calculs_max
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/lionel/calculs_max.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/deSimone.lus
@@ -7229,46 +6002,9 @@ Opening file /home/jahier/lus2lic/src/test/should_work/lionel/deSimone.lus
const deSimone::size = 10;
type deSimone::tabType = bool^10;
type deSimone::cell_accu = deSimone::cell_accu {token : bool; grant : bool};
-*** Error in file "should_work/lionel/deSimone.lus", line 51, col 23 to 30, token 'deSimone': type error:
-*** arity error: 2 argument(s) are expected, whereas 1 is/are provided
-
-node deSimone::oneCell(
- accu_in:deSimone::cell_accu;
- req:bool)
-returns (
- accu_out:deSimone::cell_accu;
- ackout:bool);
-let
- ackout = (((req and accu_in.token) and accu_in.grant) and not(false ->
- pre(ackout)));
- accu_out = cell_accu{token=accu_in.token;grant=(not(req) and
- accu_in.grant)};
-tel
--- end of node deSimone::oneCell
-
-node deSimone::prop1_iter(
- accu_in:int;
- elt_in:bool)
-returns (
- accu_out:int);
-let
- accu_out = (accu_in + if (elt_in) then (1) else (0));
-tel
--- end of node deSimone::prop1_iter
-
-node deSimone::deSimone(
- new_token:bool;
- request:bool^10)
-returns (
- acknowledge:bool^10);
-var
- accu_out:deSimone::cell_accu;
-let
- (accu_out, acknowledge) = fillred<<node deSimone::oneCell, const
- 10>>(cell_accu{token=new_token;grant=true}, request);
-tel
--- end of node deSimone::deSimone
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/lionel/deSimone.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/iterFibo.lus
@@ -7280,13 +6016,9 @@ let
elt = (accu_in[0] + accu_in[1]);
tel
-- end of node iterFibo::fibo
-node iterFibo::iterFibo(x:int; y:int) returns (T:int^10);
-var
- bidon:int^2;
-let
- (bidon, T) = fill<<node iterFibo::fibo, const 10>>([x, y]);
-tel
--- end of node iterFibo::iterFibo
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/iterFibo.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/mapiter.lus
@@ -7316,40 +6048,9 @@ let
(sacc, out) = Lustre::fill<<node mapiter::bitalt, const 2>>(in);
tel
-- end of node mapiter::fill_bitalt
-node mapiter::initmat(iacc:bool) returns (sacc:bool; R:bool^2^3);
-let
- (sacc, R) = fill<<node mapiter::fill_bitalt, const 3>>(iacc);
-tel
--- end of node mapiter::initmat
-function mapiter::red_incr(init:int; b:bool^2) returns (res:int);
-let
- res = Lustre::red<<node mapiter::incr, const 2>>(init, b);
-tel
--- end of node mapiter::red_incr
-node mapiter::reducemat(iacc:int; I:bool^2^3) returns (res:int);
-let
- res = red<<node mapiter::red_incr, const 3>>(iacc, I);
-tel
--- end of node mapiter::reducemat
-node mapiter::composemat(i1:bool^2^3; i2:bool^2^3) returns (s1:bool^2^3);
-let
- s1 = map<<node mapiter::map_egal, const 3>>(i1, i2);
-tel
--- end of node mapiter::composemat
-node mapiter::mapiter(a:bool) returns (nbTrue:int);
-var
- bid1:bool;
- bid2:bool;
- init1:bool^2^3;
- init2:bool^2^3;
- XORMAT:bool^2^3;
-let
- (bid1, init1) = mapiter::initmat(a);
- (bid2, init2) = mapiter::initmat(not(a));
- XORMAT = mapiter::composemat(init1, init2);
- nbTrue = mapiter::reducemat(0, XORMAT);
-tel
--- end of node mapiter::mapiter
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/mapiter.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/matrice.lus
@@ -7363,57 +6064,27 @@ let
elt = (accu_in[0] + accu_in[1]);
tel
-- end of node matrice::fibo
-node matrice::matrice(a:int) returns (sum:int; bid:int^2; T:int^3^2);
-let
- (bid, T) = fill<<node Lustre::fill<<node matrice::fibo, const 3>>, const
- 2>>([a, a]);
- sum = red<<node Lustre::red<<node Lustre::+, const 3>>, const 2>>(0, T);
-tel
--- end of node matrice::matrice
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/matrice.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/matrice2.lus
Opening file /home/jahier/lus2lic/src/test/should_work/lionel/matrice2.lus
const matrice2::m = 2;
const matrice2::n = 2;
-node matrice2::matrice2(a:int) returns (res:int);
-let
- res = red<<node Lustre::red<<node Lustre::+, const 2>>, const 2>>(0,
- 1^2^2);
-tel
--- end of node matrice2::matrice2
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/matrice2.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/minus.lus
Opening file /home/jahier/lus2lic/src/test/should_work/lionel/minus.lus
const minus::m = 2;
const minus::n = 3;
-node minus::bitalt(a:bool) returns (out:bool; b:bool);
-let
- b = a;
- out = not(a);
-tel
--- end of node minus::bitalt
-node minus::minus(
- a:bool^3^2;
- b:bool^3^2;
- c:bool^3^2)
-returns (
- r:bool;
- T1:bool^3^2;
- T2:bool^3^2);
-var
- bid:bool;
-let
- T1 = map<<node Lustre::map<<node Lustre::if, const 3>>, const 2>>(a, b,
- c);
- (bid, T2) = fill<<node Lustre::fill<<node minus::bitalt, const 3>>, const
- 2>>(a[0][0]);
- r = red<<node Lustre::red<<node Lustre::xor, const 3>>, const 2>>(a[0][0],
- T1);
-tel
--- end of node minus::minus
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/minus.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/moyenne.lus
@@ -7421,25 +6092,8 @@ Opening file /home/jahier/lus2lic/src/test/should_work/lionel/moyenne.lus
type moyenne::moyenne_accu = moyenne::moyenne_accu {sum : real; moyenne : real; rank : real};
const moyenne::size = 10;
-node moyenne::moyenne_step(
- accu_in:moyenne::moyenne_accu;
- elt_in:real)
-returns (
- accu_out:moyenne::moyenne_accu);
-let
- accu_out = moyenne_accu{sum=(accu_in.sum + elt_in);moyenne=((accu_in.sum +
- elt_in) / (accu_in.rank + 1.0));rank=(accu_in.rank + 1.0)};
-tel
--- end of node moyenne::moyenne_step
-node moyenne::moyenne(Tab:real^10) returns (moy:real);
-var
- accu_out:moyenne::moyenne_accu;
-let
- accu_out = red<<node moyenne::moyenne_step, const
- 10>>(moyenne_accu{sum=0.0;moyenne=0.0;rank=0.0}, Tab);
- moy = accu_out.moyenne;
-tel
--- end of node moyenne::moyenne
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/lionel/moyenne.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/normal.lus
@@ -7464,315 +6118,8 @@ const normal::EC_DELESTAGE = 4;
const normal::EC_ON = 0;
const normal::COM_ERR = 0;
-node normal::int2InfoChgIndiv(
- m:int)
-returns (
- InfoChgIndiv:normal::T_InfoChgIndiv);
-let
- InfoChgIndiv = T_InfoChgIndiv{mesure_chg=m};
-tel
--- end of node normal::int2InfoChgIndiv
-
-node normal::extract_tab_info_chg_indiv(
- EntreeGlob:normal::T_EntreeGlob)
-returns (
- TabInfoChgIndiv:normal::T_InfoChgIndiv^20);
-let
- TabInfoChgIndiv = map<<node normal::int2InfoChgIndiv, const
- 20>>(EntreeGlob.mesure_chgs);
-tel
--- end of node normal::extract_tab_info_chg_indiv
-
-node normal::int2InfoGenIndiv(
- m:int)
-returns (
- InfoGenIndiv:normal::T_InfoGenIndiv);
-let
- InfoGenIndiv = T_InfoGenIndiv{mesure_gen=m};
-tel
--- end of node normal::int2InfoGenIndiv
-
-node normal::extract_tab_info_gen_indiv(
- EntreeGlob:normal::T_EntreeGlob)
-returns (
- TabInfoGenIndiv:normal::T_InfoGenIndiv^4);
-let
- TabInfoGenIndiv = map<<node normal::int2InfoGenIndiv, const
- 4>>(EntreeGlob.mesure_gens);
-tel
--- end of node normal::extract_tab_info_gen_indiv
-node normal::egal_indice(indice:int; val:int) returns (r:bool);
-let
- r = (val = indice);
-tel
--- end of node normal::egal_indice
-node normal::copie(acc_in:int) returns (acc_out:int; elt:int);
-let
- acc_out = acc_in;
- elt = acc_in;
-tel
--- end of node normal::copie
-
-node normal::essai_traite_gen(
- indice_gen:int;
- infoGenGlob:normal::T_InfoGenGlob)
-returns (
- TabComVal:bool^20);
-var
- Tab_indiceGen:int^20;
- bid:int;
-let
- (bid, Tab_indiceGen) = fill<<node normal::copie, const 20>>(indice_gen);
- TabComVal = map<<node normal::egal_indice, const 20>>(Tab_indiceGen,
- infoGenGlob.chg2gen);
-tel
--- end of node normal::essai_traite_gen
-
-node normal::fusion_une_com(
- in_com:int;
- cur_com:int;
- cur_val:bool)
-returns (
- out_com:int);
-let
- out_com = if (cur_val) then (cur_com) else (in_com);
-tel
--- end of node normal::fusion_une_com
-
-node normal::fusion_tab_com(
- acc_in:int^20;
- TabCom:int^20;
- TabVal:bool^20)
-returns (
- acc_out:int^20);
-let
- acc_out = map<<node normal::fusion_une_com, const 20>>(acc_in, TabCom,
- TabVal);
-tel
--- end of node normal::fusion_tab_com
-
-node normal::fusion_com(
- AllTabComChg:int^20^4;
- AllTabComVal:bool^20^4)
-returns (
- TabComChg:int^20);
-var
- Vide:int^20;
-let
- Vide = COM_ERR^20;
- TabComChg = red<<node normal::fusion_tab_com, const 4>>(Vide,
- AllTabComChg, AllTabComVal);
-tel
--- end of node normal::fusion_com
-
-node normal::traite_genCore_itere(
- acc_in:int;
- elt1:bool;
- elt2:int)
-returns (
- acc_out:int;
- elt:int);
-let
- elt = if (elt1) then (elt2) else (acc_in);
- acc_out = acc_in;
-tel
--- end of node normal::traite_genCore_itere
-
-node normal::essai2(
- a:int^20;
- d:normal::T_InfoGenGlob)
-returns (
- c:bool^20);
-let
- c = map<<node normal::egal_indice, const 20>>(a, d.chg2gen);
-tel
--- end of node normal::essai2
-node normal::id(elt_in:int) returns (elt_out:int);
-let
- elt_out = elt_in;
-tel
--- end of node normal::id
-
-node normal::extract_info_chg_glob(
- EntreeGlob:normal::T_EntreeGlob)
-returns (
- InfoChgGlob:normal::T_InfoChgGlob);
-let
- InfoChgGlob = T_InfoChgGlob{chg2gen=map<<node normal::id, const
- 20>>(EntreeGlob.chg2gen)};
-tel
--- end of node normal::extract_info_chg_glob
-
-node normal::extrCharge(
- EntreeGlob:normal::T_EntreeGlob)
-returns (
- TabInfoChgIndiv:normal::T_InfoChgIndiv^20;
- TabInfoChgGlob:normal::T_InfoChgGlob^20);
-let
- TabInfoChgIndiv = normal::extract_tab_info_chg_indiv(EntreeGlob);
- TabInfoChgGlob = normal::extract_info_chg_glob(EntreeGlob)^20;
-tel
--- end of node normal::extrCharge
-node normal::trChItere(acc_in:int; elt:int) returns (acc_out:int);
-let
- acc_out = if ((acc_in > elt)) then (acc_in) else (elt);
-tel
--- end of node normal::trChItere
-
-node normal::essai3(
- indice:int^20;
- info:normal::T_InfoGenGlob)
-returns (
- Connerie:bool^20);
-let
- Connerie = map<<node normal::egal_indice, const 20>>(indice,
- info.chg2gen);
-tel
--- end of node normal::essai3
-
-node normal::traite_gen_core(
- indice_gen:int;
- InfoGenIndiv:normal::T_InfoGenIndiv;
- InfoGenGlob:normal::T_InfoGenGlob;
- TabEtatCharge:int^20;
- TabComVal:bool^20)
-returns (
- TabComChg:int^20);
-var
- bidon:int;
-let
- (bidon, TabComChg) = fillred<<node normal::traite_genCore_itere, const
- 20>>(indice_gen, TabComVal, InfoGenGlob.chg2gen);
-tel
--- end of node normal::traite_gen_core
-
-node normal::traite_gen(
- indice_gen:int;
- InfoGenIndiv:normal::T_InfoGenIndiv;
- InfoGenGlob:normal::T_InfoGenGlob;
- TabEtatCharge:int^20)
-returns (
- TabComChg:int^20;
- TabComVal:bool^20);
-var
- TabComVal_bis:bool^20;
- TabIndiceGen:int^20;
- bid:int;
-let
- TabComVal_bis = map<<node normal::egal_indice, const 20>>(TabIndiceGen,
- InfoGenGlob.chg2gen);
- (bid, TabIndiceGen) = fill<<node normal::copie, const 20>>(indice_gen);
- TabComChg = normal::traite_gen_core(indice_gen, InfoGenIndiv, InfoGenGlob,
- TabEtatCharge, TabComVal_bis);
- TabComVal = map<<node normal::egal_indice, const 20>>(TabIndiceGen,
- InfoGenGlob.chg2gen);
-tel
--- end of node normal::traite_gen
-
-node normal::extract_info_gen_glob(
- EntreeGlob:normal::T_EntreeGlob)
-returns (
- InfoGenGlob:normal::T_InfoGenGlob);
-let
- InfoGenGlob = T_InfoGenGlob{elt_bidon=0;chg2gen=map<<node normal::id,
- const 20>>(EntreeGlob.chg2gen)};
-tel
--- end of node normal::extract_info_gen_glob
-
-node normal::traite_charge(
- InfoChgIndiv:normal::T_InfoChgIndiv;
- InfoChgGlob:normal::T_InfoChgGlob)
-returns (
- EtatCharge:int);
-let
- EtatCharge = red<<node normal::trChItere, const
- 20>>(InfoChgIndiv.mesure_chg, InfoChgGlob.chg2gen);
-tel
--- end of node normal::traite_charge
-node normal::incr_acc(acc_in:int) returns (acc_out:int; res:int);
-let
- res = acc_in;
- acc_out = (res + 1);
-tel
--- end of node normal::incr_acc
-
-node normal::extrGen(
- EntreeGlob:normal::T_EntreeGlob)
-returns (
- TabInfoGenIndiv:normal::T_InfoGenIndiv^4;
- TabInfoGenGlob:normal::T_InfoGenGlob^4;
- TabIndiceGen:int^4);
-var
- bid:int;
-let
- TabInfoGenIndiv = normal::extract_tab_info_gen_indiv(EntreeGlob);
- TabInfoGenGlob = normal::extract_info_gen_glob(EntreeGlob)^4;
- (bid, TabIndiceGen) = fill<<node normal::incr_acc, const 4>>(0);
-tel
--- end of node normal::extrGen
-
-node normal::traiteGen(
- TabIndiceGen:int^4;
- TabInfoGenIndiv:normal::T_InfoGenIndiv^4;
- TabInfoGenGlob:normal::T_InfoGenGlob^4;
- TabEtatCharge:int^20)
-returns (
- AllTabComChg:int^20^4;
- AllTabComVal:bool^20^4);
-let
- (AllTabComChg, AllTabComVal) = map<<node normal::traite_gen, const
- 4>>(TabIndiceGen, TabInfoGenIndiv, TabInfoGenGlob, TabEtatCharge^4);
-tel
--- end of node normal::traiteGen
-
-node normal::traiteChg(
- TabInfoChgIndiv:normal::T_InfoChgIndiv^20;
- TabInfoChgGlob:normal::T_InfoChgGlob^20)
-returns (
- TabEtatCharge:int^20);
-let
- TabEtatCharge = map<<node normal::traite_charge, const
- 20>>(TabInfoChgIndiv, TabInfoChgGlob);
-tel
--- end of node normal::traiteChg
-
-node normal::normal(
- EntreeGlob:normal::T_EntreeGlob)
-returns (
- TabComChg:int^20);
-var
- TabInfoChgIndiv:normal::T_InfoChgIndiv^20;
- TabInfoChgGlob:normal::T_InfoChgGlob^20;
- TabEtatCharge:int^20;
- TabInfoGenIndiv:normal::T_InfoGenIndiv^4;
- TabInfoGenGlob:normal::T_InfoGenGlob^4;
- TabIndiceGen:int^4;
- AllTabComChg:int^20^4;
- AllTabComVal:bool^20^4;
-let
- (TabInfoChgIndiv, TabInfoChgGlob) = normal::extrCharge(EntreeGlob);
- TabEtatCharge = normal::traiteChg(TabInfoChgIndiv, TabInfoChgGlob);
- (TabInfoGenIndiv, TabInfoGenGlob, TabIndiceGen) =
- normal::extrGen(EntreeGlob);
- (AllTabComChg, AllTabComVal) = normal::traiteGen(TabIndiceGen,
- TabInfoGenIndiv, TabInfoGenGlob, TabEtatCharge);
- TabComChg = normal::fusion_com(AllTabComChg, AllTabComVal);
-tel
--- end of node normal::normal
-
-node normal::traite_gen_bis(
- a:int;
- c:normal::T_InfoGenGlob)
-returns (
- e:bool^20);
-var
- loc_a:int^20;
- bid:int;
-let
- (bid, loc_a) = fill<<node normal::copie, const 20>>(a);
- e = map<<node normal::egal_indice, const 20>>(loc_a, c.chg2gen);
-tel
--- end of node normal::traite_gen_bis
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/lionel/normal.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/pipeline.lus
@@ -7790,14 +6137,9 @@ let
accu_out = elt_in;
tel
-- end of node pipeline::oneStep_pipe
-node pipeline::pipeline(in:bool^10) returns (out:bool^10);
-var
- accu_out:bool;
-let
- (accu_out, out) = fillred<<node pipeline::oneStep_pipe, const 10>>(true ->
- pre(accu_out), in);
-tel
--- end of node pipeline::pipeline
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/pipeline.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/predefOp.lus
@@ -7819,95 +6161,9 @@ let
oacc = not(res);
tel
-- end of node predefOp::bitalt
-node predefOp::initmatbool(iacc:bool) returns (sacc:bool; R:bool^2^3);
-let
- (sacc, R) = fill<<node Lustre::fill<<node predefOp::bitalt, const 2>>,
- const 3>>(iacc);
-tel
--- end of node predefOp::initmatbool
-
-node predefOp::composematbool(
- i1:bool^2^3;
- i2:bool^2^3)
-returns (
- s1:bool^2^3);
-let
- s1 = map<<node Lustre::map<<node Lustre::=>, const 2>>, const 3>>(i1, i2);
-tel
--- end of node predefOp::composematbool
-node predefOp::reducematbool(iacc:int; I:bool^2^3) returns (res:int);
-let
- res = red<<node Lustre::red<<node predefOp::incr, const 2>>, const
- 3>>(iacc, I);
-tel
--- end of node predefOp::reducematbool
-
-node predefOp::predefOp2(
- a:bool)
-returns (
- nbTrue:int;
- init1:bool^2^3;
- init2:bool^2^3;
- XORMAT:bool^2^3);
-var
- bid1:bool;
- bid2:bool;
-let
- (bid1, init1) = predefOp::initmatbool(a);
- (bid2, init2) = predefOp::initmatbool(not(a));
- XORMAT = predefOp::composematbool(init1, init2);
- nbTrue = predefOp::reducematbool(0, XORMAT);
-tel
--- end of node predefOp::predefOp2
-
-node predefOp::composematint(
- i1:int^2^3;
- i2:int^2^3)
-returns (
- s1:int^2^3;
- s2:bool^2^3);
-let
- s1 = map<<node Lustre::map<<node Lustre::/, const 2>>, const 3>>(i1, i2);
- s2 = map<<node Lustre::map<<node Lustre::>=, const 2>>, const 3>>(i1, i2);
-tel
--- end of node predefOp::composematint
-node predefOp::incremental(iacc:int) returns (oacc:int; res:int);
-let
- res = iacc;
- oacc = (res + 1);
-tel
--- end of node predefOp::incremental
-node predefOp::reducematint(iacc:int; I:int^2^3) returns (res:int);
-let
- res = red<<node Lustre::red<<node Lustre::+, const 2>>, const 3>>(iacc,
- I);
-tel
--- end of node predefOp::reducematint
-node predefOp::initmatint(iacc:int) returns (sacc:int; R:int^2^3);
-let
- (sacc, R) = fill<<node Lustre::fill<<node predefOp::incremental, const
- 2>>, const 3>>(iacc);
-tel
--- end of node predefOp::initmatint
-node predefOp::predefOp(
- a:int)
-returns (
- res:int;
- init1:int^2^3;
- init2:int^2^3;
- matres1:int^2^3;
- matres2:bool^2^3);
-var
- bid1:int;
- bid2:int;
-let
- (bid1, init1) = predefOp::initmatint(a);
- (bid2, init2) = predefOp::initmatint((a * a));
- (matres1, matres2) = predefOp::composematint(init1, init2);
- res = predefOp::reducematint(0, matres1);
-tel
--- end of node predefOp::predefOp
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/predefOp.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/redIf.lus
@@ -7917,22 +6173,18 @@ let
r = if (a) then (b) else (c);
tel
-- end of node redIf::monIf
-node redIf::redIf(a:bool; b:bool^3; c:bool^3) returns (r:bool);
-let
- r = red<<node Lustre::if, const 3>>(a, b, c);
-tel
--- end of node redIf::redIf
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/redIf.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/simpleRed.lus
Opening file /home/jahier/lus2lic/src/test/should_work/lionel/simpleRed.lus
const simpleRed::m = 3;
const simpleRed::n = 2;
-node simpleRed::simpleRed(a:int) returns (res:int);
-let
- res = red<<node Lustre::+, const 3>>(0, a^3);
-tel
--- end of node simpleRed::simpleRed
+
+*** oops: an internal error occurred in file evalClock.ml, line 344, column 4
+*** when compiling lustre program should_work/lionel/simpleRed.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/testSilus.lus
@@ -7959,263 +6211,8 @@ const testSilus::EC_DELESTAGE = 4;
const testSilus::EC_ON = 0;
const testSilus::COM_ERR = 0;
-node testSilus::int2InfoChgIndiv(
- m:int)
-returns (
- InfoChgIndiv:testSilus::T_InfoChgIndiv);
-let
- InfoChgIndiv = T_InfoChgIndiv{mesure_chg=m};
-tel
--- end of node testSilus::int2InfoChgIndiv
-
-node testSilus::extract_tab_info_chg_indiv(
- EntreeGlob:testSilus::T_EntreeGlob)
-returns (
- TabInfoChgIndiv:testSilus::T_InfoChgIndiv^20);
-let
- TabInfoChgIndiv = map<<node testSilus::int2InfoChgIndiv, const
- 20>>(EntreeGlob.mesure_chgs);
-tel
--- end of node testSilus::extract_tab_info_chg_indiv
-
-node testSilus::int2InfoGenIndiv(
- m:int)
-returns (
- InfoGenIndiv:testSilus::T_InfoGenIndiv);
-let
- InfoGenIndiv = T_InfoGenIndiv{mesure_gen=m};
-tel
--- end of node testSilus::int2InfoGenIndiv
-
-node testSilus::extract_tab_info_gen_indiv(
- EntreeGlob:testSilus::T_EntreeGlob)
-returns (
- TabInfoGenIndiv:testSilus::T_InfoGenIndiv^4);
-let
- TabInfoGenIndiv = map<<node testSilus::int2InfoGenIndiv, const
- 4>>(EntreeGlob.mesure_gens);
-tel
--- end of node testSilus::extract_tab_info_gen_indiv
-node testSilus::egal_indice(indice:int; val:int) returns (r:bool);
-let
- r = (val = indice);
-tel
--- end of node testSilus::egal_indice
-node testSilus::copie(acc_in:int) returns (acc_out:int; elt:int);
-let
- acc_out = acc_in;
- elt = acc_in;
-tel
--- end of node testSilus::copie
-
-node testSilus::fusion_une_com(
- in_com:int;
- cur_com:int;
- cur_val:bool)
-returns (
- out_com:int);
-let
- out_com = if (cur_val) then (cur_com) else (in_com);
-tel
--- end of node testSilus::fusion_une_com
-
-node testSilus::fusion_tab_com(
- acc_in:int^20;
- TabCom:int^20;
- TabVal:bool^20)
-returns (
- acc_out:int^20);
-let
- acc_out = map<<node testSilus::fusion_une_com, const 20>>(acc_in, TabCom,
- TabVal);
-tel
--- end of node testSilus::fusion_tab_com
-
-node testSilus::fusion_com(
- AllTabComChg:int^20^4;
- AllTabComVal:bool^20^4)
-returns (
- TabComChg:int^20);
-var
- Vide:int^20;
-let
- Vide = COM_ERR^20;
- TabComChg = red<<node testSilus::fusion_tab_com, const 4>>(Vide,
- AllTabComChg, AllTabComVal);
-tel
--- end of node testSilus::fusion_com
-
-node testSilus::traite_genCore_itere(
- acc_in:int;
- elt1:bool;
- elt2:int)
-returns (
- acc_out:int;
- elt:int);
-let
- elt = if (elt1) then (elt2) else (acc_in);
- acc_out = acc_in;
-tel
--- end of node testSilus::traite_genCore_itere
-node testSilus::id(elt_in:int) returns (elt_out:int);
-let
- elt_out = elt_in;
-tel
--- end of node testSilus::id
-
-node testSilus::extract_info_chg_glob(
- EntreeGlob:testSilus::T_EntreeGlob)
-returns (
- InfoChgGlob:testSilus::T_InfoChgGlob);
-let
- InfoChgGlob = T_InfoChgGlob{chg2gen=map<<node testSilus::id, const
- 20>>(EntreeGlob.chg2gen)};
-tel
--- end of node testSilus::extract_info_chg_glob
-
-node testSilus::extrCharge(
- EntreeGlob:testSilus::T_EntreeGlob)
-returns (
- TabInfoChgIndiv:testSilus::T_InfoChgIndiv^20;
- TabInfoChgGlob:testSilus::T_InfoChgGlob^20);
-let
- TabInfoChgIndiv = testSilus::extract_tab_info_chg_indiv(EntreeGlob);
- TabInfoChgGlob = testSilus::extract_info_chg_glob(EntreeGlob)^20;
-tel
--- end of node testSilus::extrCharge
-node testSilus::trChItere(acc_in:int; elt:int) returns (acc_out:int);
-let
- acc_out = if ((acc_in > elt)) then (acc_in) else (elt);
-tel
--- end of node testSilus::trChItere
-
-node testSilus::traite_gen_core(
- indice_gen:int;
- InfoGenIndiv:testSilus::T_InfoGenIndiv;
- InfoGenGlob:testSilus::T_InfoGenGlob;
- TabEtatCharge:int^20;
- TabComVal:bool^20)
-returns (
- TabComChg:int^20);
-var
- bidon:int;
-let
- (bidon, TabComChg) = fillred<<node testSilus::traite_genCore_itere, const
- 20>>(indice_gen, TabComVal, InfoGenGlob.chg2gen);
-tel
--- end of node testSilus::traite_gen_core
-
-node testSilus::traite_gen(
- indice_gen:int;
- InfoGenIndiv:testSilus::T_InfoGenIndiv;
- InfoGenGlob:testSilus::T_InfoGenGlob;
- TabEtatCharge:int^20)
-returns (
- TabComChg:int^20;
- TabComVal:bool^20);
-var
- TabIndiceGen:int^20;
- bidon:int;
-let
- TabComChg = testSilus::traite_gen_core(indice_gen, InfoGenIndiv,
- InfoGenGlob, TabEtatCharge, TabComVal);
- TabComVal = map<<node testSilus::egal_indice, const 20>>(TabIndiceGen,
- InfoGenGlob.chg2gen);
- (bidon, TabIndiceGen) = fill<<node testSilus::copie, const
- 20>>(indice_gen);
-tel
--- end of node testSilus::traite_gen
-
-node testSilus::extract_info_gen_glob(
- EntreeGlob:testSilus::T_EntreeGlob)
-returns (
- InfoGenGlob:testSilus::T_InfoGenGlob);
-let
- InfoGenGlob = T_InfoGenGlob{elt_bidon=0;chg2gen=map<<node testSilus::id,
- const 20>>(EntreeGlob.chg2gen)};
-tel
--- end of node testSilus::extract_info_gen_glob
-
-node testSilus::traite_charge(
- InfoChgIndiv:testSilus::T_InfoChgIndiv;
- InfoChgGlob:testSilus::T_InfoChgGlob)
-returns (
- EtatCharge:int);
-let
- EtatCharge = red<<node testSilus::trChItere, const
- 20>>(InfoChgIndiv.mesure_chg, InfoChgGlob.chg2gen);
-tel
--- end of node testSilus::traite_charge
-
-node testSilus::traiteChg(
- TabInfoChgIndiv:testSilus::T_InfoChgIndiv^20;
- TabInfoChgGlob:testSilus::T_InfoChgGlob^20)
-returns (
- TabEtatCharge:int^20);
-let
- TabEtatCharge = map<<node testSilus::traite_charge, const
- 20>>(TabInfoChgIndiv, TabInfoChgGlob);
-tel
--- end of node testSilus::traiteChg
-node testSilus::incr_acc(acc_in:int) returns (acc_out:int; res:int);
-let
- res = acc_in;
- acc_out = (res + 1);
-tel
--- end of node testSilus::incr_acc
-
-node testSilus::extrGen(
- EntreeGlob:testSilus::T_EntreeGlob)
-returns (
- TabInfoGenIndiv:testSilus::T_InfoGenIndiv^4;
- TabInfoGenGlob:testSilus::T_InfoGenGlob^4;
- TabIndiceGen:int^4);
-var
- bidon:int;
-let
- TabInfoGenIndiv = testSilus::extract_tab_info_gen_indiv(EntreeGlob);
- TabInfoGenGlob = testSilus::extract_info_gen_glob(EntreeGlob)^4;
- (bidon, TabIndiceGen) = fill<<node testSilus::incr_acc, const 4>>(0);
-tel
--- end of node testSilus::extrGen
-
-node testSilus::traiteGen(
- TabIndiceGen:int^4;
- TabInfoGenIndiv:testSilus::T_InfoGenIndiv^4;
- TabInfoGenGlob:testSilus::T_InfoGenGlob^4;
- TabEtatCharge:int^20)
-returns (
- AllTabComChg:int^20^4;
- AllTabComVal:bool^20^4);
-let
- (AllTabComChg, AllTabComVal) = map<<node testSilus::traite_gen, const
- 4>>(TabIndiceGen, TabInfoGenIndiv, TabInfoGenGlob, TabEtatCharge^4);
-tel
--- end of node testSilus::traiteGen
-
-node testSilus::testSilus(
- EntreeGlob:testSilus::T_EntreeGlob)
-returns (
- TabComChg:int^20);
-var
- TabInfoChgIndiv:testSilus::T_InfoChgIndiv^20;
- TabInfoChgGlob:testSilus::T_InfoChgGlob^20;
- TabEtatCharge:int^20;
- TabInfoGenIndiv:testSilus::T_InfoGenIndiv^4;
- TabInfoGenGlob:testSilus::T_InfoGenGlob^4;
- TabIndiceGen:int^4;
- AllTabComChg:int^20^4;
- AllTabComVal:bool^20^4;
-let
- (TabInfoChgIndiv, TabInfoChgGlob) = testSilus::extrCharge(EntreeGlob);
- TabEtatCharge = testSilus::traiteChg(TabInfoChgIndiv, TabInfoChgGlob);
- (TabInfoGenIndiv, TabInfoGenGlob, TabIndiceGen) =
- testSilus::extrGen(EntreeGlob);
- (AllTabComChg, AllTabComVal) = testSilus::traiteGen(TabIndiceGen,
- TabInfoGenIndiv, TabInfoGenGlob, TabEtatCharge);
- TabComChg = testSilus::fusion_com(AllTabComChg, AllTabComVal);
-tel
--- end of node testSilus::testSilus
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/lionel/testSilus.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/triSel.lus
@@ -8228,106 +6225,8 @@ type triSel::MinFR_accu = triSel::MinFR_accu {MinVal : int; MinRank : int; RankF
type triSel::sorted_iter_accu = triSel::sorted_iter_accu {prev_elt : int; prop_is_tt : bool};
type triSel::Exchange_accu = triSel::Exchange_accu {MinVal : int; MinRank : int; RankFrom : int; CurrentVal : int; Rank : int};
-node triSel::minFromRank(
- accu_in:triSel::MinFR_accu;
- TabEltIn:int)
-returns (
- accu_out:triSel::MinFR_accu);
-let
- accu_out = MinFR_accu{MinVal= if (((accu_in.Rank = 0) or (accu_in.Rank =
- accu_in.RankFrom))) then (TabEltIn) else ( if ((accu_in.Rank >=
- accu_in.RankFrom)) then ( if ((TabEltIn < accu_in.MinVal)) then (TabEltIn)
- else (accu_in.MinVal)) else (accu_in.MinVal));MinRank= if (((accu_in.Rank =
- 0) or (accu_in.Rank = accu_in.RankFrom))) then (accu_in.Rank) else ( if
- ((accu_in.Rank >= accu_in.RankFrom)) then ( if ((TabEltIn <
- accu_in.MinVal)) then (accu_in.Rank) else (accu_in.MinRank)) else
- (accu_in.MinRank));RankFrom=accu_in.RankFrom;Rank=(accu_in.Rank + 1)};
-tel
--- end of node triSel::minFromRank
-
-node triSel::select(
- accu_in:triSel::Select_accu;
- elt:int)
-returns (
- accu_out:triSel::Select_accu);
-let
- accu_out =
- Select_accu{RankToFind=accu_in.RankToFind;CurrentRank=(accu_in.CurrentRank
- + 1);Val= if ((accu_in.RankToFind = accu_in.CurrentRank)) then (elt) else
- (accu_in.Val)};
-tel
--- end of node triSel::select
-
-node triSel::Exchange_i_j(
- accu_in:triSel::Exchange_accu;
- eltIn:int)
-returns (
- accu_out:triSel::Exchange_accu;
- eltOut:int);
-let
- accu_out =
- Exchange_accu{MinVal=accu_in.MinVal;MinRank=accu_in.MinRank;RankFrom=accu_in.RankFrom;CurrentVal=accu_in.CurrentVal;Rank=(accu_in.Rank
- + 1)};
- eltOut = if ((accu_in.Rank = accu_in.MinRank)) then (accu_in.CurrentVal)
- else ( if ((accu_in.Rank = accu_in.RankFrom)) then (accu_in.MinVal) else
- (eltIn));
-tel
--- end of node triSel::Exchange_i_j
-
-node triSel::UnarySort(
- accu_in:triSel::Sort_accu;
- eltIn:int)
-returns (
- accu_out:triSel::Sort_accu);
-var
- accu_out_select:triSel::Select_accu;
- accu_out_min:triSel::MinFR_accu;
- accu_out_exchange:triSel::Exchange_accu;
- localTab:int^50;
-let
- accu_out_min = red<<node triSel::minFromRank, const
- 50>>(MinFR_accu{MinVal=0;MinRank=0;RankFrom=accu_in.CurrentRank;Rank=0},
- accu_in.Tab);
- accu_out_select = red<<node triSel::select, const
- 50>>(Select_accu{RankToFind=accu_in.CurrentRank;CurrentRank=0;Val=0},
- accu_in.Tab);
- (accu_out_exchange, localTab) = fillred<<node triSel::Exchange_i_j, const
- 50>>(Exchange_accu{MinVal=accu_out_min.MinVal;MinRank=accu_out_min.MinRank;RankFrom=accu_out_select.RankToFind;CurrentVal=accu_out_select.Val;Rank=0},
- accu_in.Tab);
- accu_out = Sort_accu{CurrentRank=(accu_in.CurrentRank + 1);Tab=localTab};
-tel
--- end of node triSel::UnarySort
-node triSel::triSel(TIn:int^50) returns (TSorted:int^50);
-var
- UnarySort_accu_out:triSel::Sort_accu;
-let
- UnarySort_accu_out = red<<node triSel::UnarySort, const
- 50>>(Sort_accu{CurrentRank=0;Tab=TIn}, TIn);
- TSorted = UnarySort_accu_out.Tab;
-tel
--- end of node triSel::triSel
-
-node triSel::sorted_iter(
- accu_in:triSel::sorted_iter_accu;
- elt:int)
-returns (
- accu_out:triSel::sorted_iter_accu);
-let
- accu_out = sorted_iter_accu{prev_elt=elt;prop_is_tt=((accu_in.prev_elt <=
- elt) and accu_in.prop_is_tt)};
-tel
--- end of node triSel::sorted_iter
-node triSel::Sorted(TIn:int^50) returns (ok:bool);
-var
- accu_out:triSel::sorted_iter_accu;
- TSorted:int^50;
-let
- TSorted = triSel::triSel(TIn);
- accu_out = red<<node triSel::sorted_iter, const
- 50>>(sorted_iter_accu{prev_elt=0;prop_is_tt=true}, TSorted);
- ok = accu_out.prop_is_tt;
-tel
--- end of node triSel::Sorted
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/lionel/triSel.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/packEnvTest/Condact.lus
@@ -8346,7 +6245,7 @@ tel
-- end of node TestCondact::n
node TestCondact::C(c:bool; d:int; x:int) returns (y:int);
let
- y = if (c) then (current (TestCondact::n(x))) else (d -> pre(y));
+ y = if (c) then (TestCondact::n(x)) else (d -> pre(y));
tel
-- end of node TestCondact::C
node Main::Condact(c:bool; d:int; x:int) returns (y:int);
@@ -8362,34 +6261,8 @@ type contractForElementSelectionInArray::elementType = int;
type contractForElementSelectionInArray::iteratedStruct = contractForElementSelectionInArray::iteratedStruct {currentRank : int; rankToSelect : int; elementSelected : int};
const contractForElementSelectionInArray::size = 10;
-node contractForElementSelectionInArray::selectOneStage(
- acc_in:contractForElementSelectionInArray::iteratedStruct;
- currentElt:int)
-returns (
- acc_out:contractForElementSelectionInArray::iteratedStruct);
-let
- acc_out = iteratedStruct{currentRank=(acc_in.currentRank +
- 1);rankToSelect=acc_in.rankToSelect;elementSelected= if
- ((acc_in.currentRank = acc_in.rankToSelect)) then (currentElt) else
- (acc_in.elementSelected)};
-tel
--- end of node contractForElementSelectionInArray::selectOneStage
-
-node contractForElementSelectionInArray::selectEltInArray(
- array:int^10;
- rankToSelect:int)
-returns (
- elementSelected:int);
-var
- iterationResult:contractForElementSelectionInArray::iteratedStruct;
-let
- iterationResult = red<<node
- contractForElementSelectionInArray::selectOneStage, const
- 10>>(iteratedStruct{currentRank=0;rankToSelect=rankToSelect;elementSelected=0},
- array);
- elementSelected = iterationResult.elementSelected;
-tel
--- end of node contractForElementSelectionInArray::selectEltInArray
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/packEnvTest/contractForElementSelectionInArray/contractForElementSelectionInArray.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/packEnvTest/contractForElementSelectionInArray/main.lus
@@ -8415,266 +6288,8 @@ tel
-- end of node intArray::_isEqualTo_
type intArray::T_isElementOf_ = intArray::T_isElementOf_ {eltToSearch : int; iselementof : bool};
-node intArray::iterated_isElementOf_(
- acc_in:intArray::T_isElementOf_;
- elt_in:int)
-returns (
- acc_out:intArray::T_isElementOf_);
-let
- acc_out =
- T_isElementOf_{eltToSearch=acc_in.eltToSearch;iselementof=(acc_in or
- intArray::_isEqualTo_(acc_in.eltToSearch, elt_in))};
-tel
--- end of node intArray::iterated_isElementOf_
-node intArray::_isElementOf_(e:int; t:int^10) returns (iselementof:bool);
-var
- acc_out:intArray::T_isElementOf_;
-let
- acc_out = red<<node intArray::iterated_isElementOf_, const
- 10>>(T_isElementOf_{eltToSearch=e;iselementof=false}, t);
- iselementof = acc_out.iselementof;
-tel
--- end of node intArray::_isElementOf_
-type intArray::forSortingAlgo = intArray::forSortingAlgo {previousElement : int; sortedUpToHere : bool};
-node intArray::_isGreaterOrEqualTo_(e1:int; e2:int) returns (ge:bool);
-let
- ge = (intArray::_isGreaterThan_(e1, e2) or intArray::_isEqualTo_(e1, e2));
-tel
--- end of node intArray::_isGreaterOrEqualTo_
-
-node intArray::isLocallyLoselySorted(
- acc_in:intArray::forSortingAlgo;
- elt:int)
-returns (
- acc_out:intArray::forSortingAlgo);
-let
- acc_out =
- forSortingAlgo{previousElement=elt;sortedUpToHere=(intArray::_isGreaterOrEqualTo_(elt,
- acc_in.previousElement) and acc_in.sortedUpToHere)};
-tel
--- end of node intArray::isLocallyLoselySorted
-
-node intArray::_isLoselySorted(
- array:int^10)
-returns (
- array_isLoselySorted:bool);
-var
- result:intArray::forSortingAlgo;
-let
- result = red<<node intArray::isLocallyLoselySorted, const
- 10>>(forSortingAlgo{previousElement=array[0];sortedUpToHere=true}, array);
- array_isLoselySorted = result.sortedUpToHere;
-tel
--- end of node intArray::_isLoselySorted
-type intArray::Sort_accu = intArray::Sort_accu {CurrentRank : int; Tab : int^10};
-type intArray::Select_accu = intArray::Select_accu {RankToFind : int; CurrentRank : int; Val : int};
-type intArray::MinFR_accu = intArray::MinFR_accu {MinVal : int; MinRank : int; RankFrom : int; Rank : int};
-type intArray::Exchange_accu = intArray::Exchange_accu {MinVal : int; MinRank : int; RankFrom : int; CurrentVal : int; Rank : int};
-
-node intArray::minFromRank(
- accu_in:intArray::MinFR_accu;
- TabEltIn:int)
-returns (
- accu_out:intArray::MinFR_accu);
-let
- accu_out = MinFR_accu{MinVal= if ((accu_in.Rank <= accu_in.RankFrom)) then
- (TabEltIn) else ( if ((accu_in.Rank >= accu_in.RankFrom)) then ( if
- ((TabEltIn < accu_in.MinVal)) then (TabEltIn) else (accu_in.MinVal)) else
- (accu_in.MinVal));MinRank= if ((accu_in.Rank > accu_in.RankFrom)) then ( if
- ((TabEltIn < accu_in.MinVal)) then (accu_in.Rank) else (accu_in.MinRank))
- else (accu_in.MinRank);RankFrom=accu_in.RankFrom;Rank=(accu_in.Rank + 1)};
-tel
--- end of node intArray::minFromRank
-
-node intArray::select(
- accu_in:intArray::Select_accu;
- elt:int)
-returns (
- accu_out:intArray::Select_accu);
-let
- accu_out =
- Select_accu{RankToFind=accu_in.RankToFind;CurrentRank=(accu_in.CurrentRank
- + 1);Val= if ((accu_in.RankToFind = accu_in.CurrentRank)) then (elt) else
- (accu_in.Val)};
-tel
--- end of node intArray::select
-
-node intArray::Exchange_i_j(
- accu_in:intArray::Exchange_accu;
- eltIn:int)
-returns (
- accu_out:intArray::Exchange_accu;
- eltOut:int);
-let
- accu_out =
- Exchange_accu{MinVal=accu_in.MinVal;MinRank=accu_in.MinRank;RankFrom=accu_in.RankFrom;CurrentVal=accu_in.CurrentVal;Rank=(accu_in.Rank
- + 1)};
- eltOut = if ((accu_in.Rank = accu_in.MinRank)) then (accu_in.CurrentVal)
- else ( if ((accu_in.Rank = accu_in.RankFrom)) then (accu_in.MinVal) else
- (eltIn));
-tel
--- end of node intArray::Exchange_i_j
-
-node intArray::UnarySort(
- accu_in:intArray::Sort_accu;
- eltIn:int)
-returns (
- accu_out:intArray::Sort_accu);
-var
- accu_out_select:intArray::Select_accu;
- accu_out_min:intArray::MinFR_accu;
- accu_out_exchange:intArray::Exchange_accu;
- localTab:int^10;
-let
- accu_out_min = red<<node intArray::minFromRank, const
- 10>>(MinFR_accu{MinVal=0;MinRank=accu_in.CurrentRank;RankFrom=accu_in.CurrentRank;Rank=0},
- accu_in.Tab);
- accu_out_select = red<<node intArray::select, const
- 10>>(Select_accu{RankToFind=accu_in.CurrentRank;CurrentRank=0;Val=0},
- accu_in.Tab);
- (accu_out_exchange, localTab) = fillred<<node intArray::Exchange_i_j,
- const
- 10>>(Exchange_accu{MinVal=accu_out_min.MinVal;MinRank=accu_out_min.MinRank;RankFrom=accu_out_select.RankToFind;CurrentVal=accu_out_select.Val;Rank=0},
- accu_in.Tab);
- accu_out = Sort_accu{CurrentRank=(accu_in.CurrentRank + 1);Tab=localTab};
-tel
--- end of node intArray::UnarySort
-node intArray::sort_(array:int^10) returns (arraySorted:int^10);
-var
- UnarySort_accu_out:intArray::Sort_accu;
-let
- UnarySort_accu_out = red<<node intArray::UnarySort, const
- 10>>(Sort_accu{CurrentRank=0;Tab=array}, array);
- arraySorted = UnarySort_accu_out.Tab;
-tel
--- end of node intArray::sort_
-node intArray::selectMax(e1:int; e2:int) returns (e:int);
-let
- e = if (intArray::_isGreaterThan_(e1, e2)) then (e1) else (e2);
-tel
--- end of node intArray::selectMax
-node intArray::getMaximumIn_(array:int^10) returns (maximumElement:int);
-let
- maximumElement = red<<node intArray::selectMax, const 10>>(array[0],
- array);
-tel
--- end of node intArray::getMaximumIn_
-type intArray::iteratedStruct = intArray::iteratedStruct {currentRank : int; rankToSelect : int; elementSelected : int};
-
-node intArray::selectOneStage(
- acc_in:intArray::iteratedStruct;
- currentElt:int)
-returns (
- acc_out:intArray::iteratedStruct);
-let
- acc_out = iteratedStruct{currentRank=(acc_in.currentRank +
- 1);rankToSelect=acc_in.rankToSelect;elementSelected= if
- ((acc_in.currentRank = acc_in.rankToSelect)) then (currentElt) else
- (acc_in.elementSelected)};
-tel
--- end of node intArray::selectOneStage
-
-node intArray::selectElementOfRank_inArray_(
- rankToSelect:int;
- array:int^10)
-returns (
- elementSelected:int);
-var
- iterationResult:intArray::iteratedStruct;
-let
- iterationResult = red<<node intArray::selectOneStage, const
- 10>>(iteratedStruct{currentRank=0;rankToSelect=rankToSelect;elementSelected=array[0]},
- array);
- elementSelected = iterationResult.elementSelected;
-tel
--- end of node intArray::selectElementOfRank_inArray_
-node intArray::selectMin(e1:int; e2:int) returns (e:int);
-let
- e = if (intArray::_isGreaterThan_(e1, e2)) then (e2) else (e1);
-tel
--- end of node intArray::selectMin
-node intArray::getMinimumIn_(array:int^10) returns (minimumElement:int);
-var
- maximum:int;
-let
- maximum = intArray::getMaximumIn_(array);
- minimumElement = red<<node intArray::selectMin, const 10>>(maximum,
- array);
-tel
--- end of node intArray::getMinimumIn_
-type intArray::currentRank_withMemorizedRank = intArray::currentRank_withMemorizedRank {currentRank : int; rankOfMemorizedVal : int; memorizedVal : int};
-
-node intArray::selectMaxRank(
- acc_in:intArray::currentRank_withMemorizedRank;
- e1:int)
-returns (
- acc_out:intArray::currentRank_withMemorizedRank);
-let
- acc_out = currentRank_withMemorizedRank{currentRank=(acc_in.currentRank +
- 1);rankOfMemorizedVal= if (intArray::_isGreaterThan_(e1,
- acc_in.memorizedVal)) then (acc_in.currentRank) else
- (acc_in.rankOfMemorizedVal);memorizedVal= if (intArray::_isGreaterThan_(e1,
- acc_in.memorizedVal)) then (e1) else (acc_in.memorizedVal)};
-tel
--- end of node intArray::selectMaxRank
-
-node intArray::getRank_ofMaximumIn_(
- array:int^10)
-returns (
- rankOfMaximumElement:int);
-var
- local:intArray::currentRank_withMemorizedRank;
-let
- local = red<<node intArray::selectMaxRank, const
- 10>>(currentRank_withMemorizedRank{currentRank=0;rankOfMemorizedVal=0;memorizedVal=array[0]},
- array);
- rankOfMaximumElement = local.rankOfMemorizedVal;
-tel
--- end of node intArray::getRank_ofMaximumIn_
-
-node intArray::selectMinRank(
- acc_in:intArray::currentRank_withMemorizedRank;
- elt:int)
-returns (
- acc_out:intArray::currentRank_withMemorizedRank);
-let
- acc_out = currentRank_withMemorizedRank{currentRank=(acc_in.currentRank +
- 1);rankOfMemorizedVal= if (intArray::_isEqualTo_(acc_in.memorizedVal, elt))
- then (acc_in.currentRank) else
- (acc_in.rankOfMemorizedVal);memorizedVal=acc_in.memorizedVal};
-tel
--- end of node intArray::selectMinRank
-
-node intArray::getRank_ofMinimumIn_(
- array:int^10)
-returns (
- rankOfMinimumElement:int);
-var
- minElement:int;
-let
- minElement = intArray::getMinimumIn_(array);
- rankOfMinimumElement = red<<node intArray::selectMinRank, const
- 10>>(currentRank_withMemorizedRank{currentRank=0;rankOfMemorizedVal=0;memorizedVal=minElement},
- array).rankOfMemorizedVal;
-tel
--- end of node intArray::getRank_ofMinimumIn_
-
-node main::main(
- a:int^10)
-returns (
- tri:int^10;
- pos_min:int;
- min:int;
- pos_max:int;
- max:int);
-let
- min = intArray::getMinimumIn_(a);
- pos_min = intArray::getRank_ofMinimumIn_(a);
- max = intArray::getMaximumIn_(a);
- pos_max = intArray::getRank_ofMaximumIn_(a);
- tri = intArray::sort_(a);
-tel
--- end of node main::main
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/packEnvTest/contractForElementSelectionInArray/main.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/packEnvTest/contractForElementSelectionInArray/noeudsIndependants.lus
@@ -8706,105 +6321,8 @@ type tri::MinFR_accu = tri::MinFR_accu {MinVal : int; MinRank : int; RankFrom :
type tri::sorted_iter_accu = tri::sorted_iter_accu {prev_elt : int; prop_is_tt : bool};
type tri::Exchange_accu = tri::Exchange_accu {MinVal : int; MinRank : int; RankFrom : int; CurrentVal : int; Rank : int};
-node tri::minFromRank(
- accu_in:tri::MinFR_accu;
- TabEltIn:int)
-returns (
- accu_out:tri::MinFR_accu);
-let
- accu_out = MinFR_accu{MinVal= if ((accu_in.Rank <= accu_in.RankFrom)) then
- (TabEltIn) else ( if ((accu_in.Rank >= accu_in.RankFrom)) then ( if
- ((TabEltIn < accu_in.MinVal)) then (TabEltIn) else (accu_in.MinVal)) else
- (accu_in.MinVal));MinRank= if ((accu_in.Rank > accu_in.RankFrom)) then ( if
- ((TabEltIn < accu_in.MinVal)) then (accu_in.Rank) else (accu_in.MinRank))
- else (accu_in.MinRank);RankFrom=accu_in.RankFrom;Rank=(accu_in.Rank + 1)};
-tel
--- end of node tri::minFromRank
-
-node tri::select(
- accu_in:tri::Select_accu;
- elt:int)
-returns (
- accu_out:tri::Select_accu);
-let
- accu_out =
- Select_accu{RankToFind=accu_in.RankToFind;CurrentRank=(accu_in.CurrentRank
- + 1);Val= if ((accu_in.RankToFind = accu_in.CurrentRank)) then (elt) else
- (accu_in.Val)};
-tel
--- end of node tri::select
-
-node tri::Exchange_i_j(
- accu_in:tri::Exchange_accu;
- eltIn:int)
-returns (
- accu_out:tri::Exchange_accu;
- eltOut:int);
-let
- accu_out =
- Exchange_accu{MinVal=accu_in.MinVal;MinRank=accu_in.MinRank;RankFrom=accu_in.RankFrom;CurrentVal=accu_in.CurrentVal;Rank=(accu_in.Rank
- + 1)};
- eltOut = if ((accu_in.Rank = accu_in.MinRank)) then (accu_in.CurrentVal)
- else ( if ((accu_in.Rank = accu_in.RankFrom)) then (accu_in.MinVal) else
- (eltIn));
-tel
--- end of node tri::Exchange_i_j
-
-node tri::UnarySort(
- accu_in:tri::Sort_accu;
- eltIn:int)
-returns (
- accu_out:tri::Sort_accu);
-var
- accu_out_select:tri::Select_accu;
- accu_out_min:tri::MinFR_accu;
- accu_out_exchange:tri::Exchange_accu;
- localTab:int^10;
-let
- accu_out_min = red<<node tri::minFromRank, const
- 10>>(MinFR_accu{MinVal=0;MinRank=accu_in.CurrentRank;RankFrom=accu_in.CurrentRank;Rank=0},
- accu_in.Tab);
- accu_out_select = red<<node tri::select, const
- 10>>(Select_accu{RankToFind=accu_in.CurrentRank;CurrentRank=0;Val=0},
- accu_in.Tab);
- (accu_out_exchange, localTab) = fillred<<node tri::Exchange_i_j, const
- 10>>(Exchange_accu{MinVal=accu_out_min.MinVal;MinRank=accu_out_min.MinRank;RankFrom=accu_out_select.RankToFind;CurrentVal=accu_out_select.Val;Rank=0},
- accu_in.Tab);
- accu_out = Sort_accu{CurrentRank=(accu_in.CurrentRank + 1);Tab=localTab};
-tel
--- end of node tri::UnarySort
-node tri::main(TIn:int^10) returns (TSorted:int^10);
-var
- UnarySort_accu_out:tri::Sort_accu;
-let
- UnarySort_accu_out = red<<node tri::UnarySort, const
- 10>>(Sort_accu{CurrentRank=0;Tab=[7, 8, 4, 3, 2, 9, 1, 10, 2, 7]}, [7, 8,
- 4, 3, 2, 9, 1, 10, 2, 7]);
- TSorted = UnarySort_accu_out.Tab;
-tel
--- end of node tri::main
-
-node tri::sorted_iter(
- accu_in:tri::sorted_iter_accu;
- elt:int)
-returns (
- accu_out:tri::sorted_iter_accu);
-let
- accu_out = sorted_iter_accu{prev_elt=elt;prop_is_tt=((accu_in.prev_elt <=
- elt) and accu_in.prop_is_tt)};
-tel
--- end of node tri::sorted_iter
-node tri::Sorted(TIn:int^10) returns (res:bool);
-var
- accu_out:tri::sorted_iter_accu;
- TSorted:int^10;
-let
- TSorted = tri::main(TIn);
- accu_out = red<<node tri::sorted_iter, const
- 10>>(sorted_iter_accu{prev_elt=0;prop_is_tt=true}, TSorted);
- res = accu_out.prop_is_tt;
-tel
--- end of node tri::Sorted
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/packEnvTest/contractForElementSelectionInArray/tri.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/packEnvTest/modelInst.lus
@@ -8866,26 +6384,8 @@ tel
-- end of node pint::fby1
type inter::selType = inter::selType {i : int; b : bool; r : real};
-node inter::preced(
- in:inter::selType)
-returns (
- out:inter::selType;
- out2:inter::selType);
-let
- out2 = selType{i=0;b=true;r=0.};
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
-tel
--- end of node inter::preced
-node mainPack::preced(in:inter::selType) returns (out:inter::selType);
-var
- out2:inter::selType;
-let
- (out, out2) = inter::preced(in);
-tel
--- end of node mainPack::preced
-const inter::n = -4;
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/packEnvTest/packages.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/packEnvTest/packages2.lus
@@ -8911,23 +6411,8 @@ tel
type inter::selType = inter::selType {i : int; b : bool; r : real};
const inter::n = -4;
-node inter::preced(
- in:inter::selType)
-returns (
- out:inter::selType;
- out2:inter::selType);
-let
- out2 = selType{i=0;b=true;r=0.};
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
-tel
--- end of node inter::preced
-node main::foo(in:int) returns (out:int);
-let
- out = in;
-tel
--- end of node main::foo
+*** oops: an internal error occurred in file evalClock.ml, line 358, column 27
+*** when compiling lustre program should_work/packEnvTest/packages2.lus
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/to_sort_out/asservi.lus
@@ -9010,6 +6495,15 @@ tel
-- end of node asservi::asservi
Those tests are supposed to generate errors
+----------------------------------------------------------------------
+====> ../lus2lic -vl 2 --compile-all-items should_fail/clock/bad_call02.lus
+Opening file /home/jahier/lus2lic/src/test/should_fail/clock/bad_call02.lus
+*** Error in file "should_fail/clock/bad_call02.lus", line 6, col 4 to 4, token '=':
+*** clock error: The expression has clock ' on base',
+*** but it is used with clock ' on c on base'.
+
+
+
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_fail/clock/clock.lus
Opening file /home/jahier/lus2lic/src/test/should_fail/clock/clock.lus
diff --git a/src/unifyClock.ml b/src/unifyClock.ml
new file mode 100644
index 00000000..f0230196
--- /dev/null
+++ b/src/unifyClock.ml
@@ -0,0 +1,119 @@
+(** Time-stamp: <modified the 26/06/2008 (at 15:17) by Erwan Jahier> *)
+
+
+open SyntaxTree
+open SyntaxTreeCore
+open CompiledData
+open CompiledDataDump
+open Printf
+open Lxm
+open Errors
+
+(* exported *)
+type clock_info =
+ | Ci_base
+ | Ci_on of var_info_eff * clock_info
+ | Ci_var of int (* to deal with polymorphic clocks (i.e., constants) *)
+
+(* exported *)
+let rec (var_info_eff_to_clock_info:var_info_eff -> clock_info) =
+ fun v ->
+ match v.var_clock_eff with
+ | BaseEff -> Ci_on(v, Ci_base)
+ | On clk -> Ci_on(v, var_info_eff_to_clock_info clk)
+
+let rec (string_of_clock_info:clock_info -> string) = function
+ | Ci_var i -> "'a" ^ string_of_int i
+ | Ci_base -> "base"
+ | Ci_on (v,clk) -> " on " ^ (aux clk)
+and aux = function
+ | Ci_var i -> "'a" ^ string_of_int i
+ | Ci_base -> "base"
+ | Ci_on (v,clk) -> (Ident.to_string v.var_name_eff) ^ " on " ^ (aux clk)
+
+let ci2str = string_of_clock_info
+
+(* exported *)
+type subst =
+ (var_info_eff * var_info_eff) list * (int * clock_info) list
+
+(* exported *)
+let (empty_subst:subst) = [],[]
+
+
+let subst_to_string (s1,s2) =
+ let v2s v = Ident.to_string v.var_name_eff 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 -> clock_info -> clock_info) =
+ fun (s1,s2) c ->
+ match c with
+ | Ci_base -> Ci_base
+ | Ci_on(v,clk) ->
+ let v = try List.assoc v s1 with Not_found -> v in
+ Ci_on(v, apply_subst (s1,s2) clk)
+ | Ci_var i ->
+ try apply_subst (s1,s2) (List.assoc i s2)
+ with Not_found -> c
+
+(* exported *)
+let (f : Lxm.t -> subst -> clock_info -> clock_info -> subst) =
+ fun lxm (s1,s2) ci1 ci2 ->
+ let ci1 = apply_subst (s1,s2) ci1 in
+ let ci2 = apply_subst (s1,s2) ci2 in
+ let rec aux (s1,s2) arg = match arg with
+ | Ci_on(v,clk), Ci_base
+ | Ci_base, Ci_on(v,clk) -> (s1,s2)
+ (* not unifiable: we stop trying to find a substitution and return s;
+ the error message will be issued outside [aux].
+ *)
+ | Ci_base, Ci_base -> (s1,s2) (* ok *)
+ | Ci_on(v1,clk1), Ci_on(v2,clk2) ->
+ let s1 = if v1 = v2 then s1 else ((v2,v1)::s1) in
+ aux (s1,s2) (clk1, clk2)
+ | Ci_var i, Ci_var j -> if i<>j then s1,((i,Ci_var j)::s2) else s1,s2
+ | Ci_var i, ci
+ | ci, Ci_var i -> s1,((i,ci)::s2)
+ in
+ let s = aux (s1,s2) (ci1,ci2) in
+ let unifiable =
+ (* two clocks are unifiable iff, once s have been applied, they are
+ equal modulo the left-most hand-side *)
+ match apply_subst s ci1, apply_subst s ci2 with
+ | Ci_on(_,c1),Ci_on(_,c2) -> c1 = c2
+ | Ci_base, Ci_base -> true
+ | Ci_base,Ci_on(_,_)
+ | Ci_on(_,_),Ci_base -> false
+ | Ci_var _, _
+ | _, Ci_var _ -> true
+ in
+ if unifiable then (
+ Verbose.print_string ~level:3 (
+ "# clock checking: unifying '" ^ (ci2str ci1) ^
+ "' and '" ^ (ci2str ci2) ^ "' -> "^ (subst_to_string s) ^"\n");
+ flush stdout;
+ s
+ )
+ else
+ let msg =
+ "\n*** clock error: The expression has clock '" ^
+ (ci2str ci1) ^ "', \n*** but it is used with clock '" ^
+ (ci2str ci2) ^ "'.\n"
+ in
+ raise(Compile_error(lxm, msg))
+
+(* exported *)
+let (list : Lxm.t -> clock_info list -> subst -> clock_info * subst) =
+ fun lxm cl s ->
+ List.fold_left
+ (fun (clk,s) clk2 ->
+ let s = f lxm s clk clk2 in
+ let clk = apply_subst s clk in (* necessary? *)
+ (clk,s)
+ )
+ (List.hd cl, s)
+ (List.tl cl)
diff --git a/src/unifyClock.mli b/src/unifyClock.mli
new file mode 100644
index 00000000..8abed5e9
--- /dev/null
+++ b/src/unifyClock.mli
@@ -0,0 +1,48 @@
+(** Time-stamp: <modified the 26/06/2008 (at 15:16) by Erwan Jahier> *)
+
+open CompiledData
+
+type clock_info =
+ | Ci_base
+ | Ci_on of var_info_eff * clock_info
+ | Ci_var of int (* to deal with polymorphic clocks (i.e., constants) *)
+
+
+(** a few conversion function *)
+
+val var_info_eff_to_clock_info:var_info_eff -> clock_info
+val string_of_clock_info:clock_info -> string
+
+
+(* XXX use Map.t
+
+ We have Two kind of substitutions.
+
+ - One is used to deal with the clock name binding, to relate node
+ parameters and node arguments.
+
+ - The other one is used to deal with polymorphic clock
+ variables. Indeed, constant clock is intrinsically
+ polymorphic. Hence, when clocking a contant (e.g., "42"), we
+ return the clock_info Ci_var i, where i is a fresh
+ integer. Afterwards, when encoutering an expression such as
+ "42+x", where we know the clock of x (clk_x), we produce the
+ substitution (i,clk_x).
+
+ XXX Shouldn't I merge the 2 kind of substitutions ? That would
+ mean I need to invent a fake var_info_eff, but it would make the
+ more homogeous.
+
+ XXX Make it abstract
+*)
+type subst =
+ (var_info_eff * var_info_eff) list * (int * clock_info) list
+
+val empty_subst : subst
+
+
+val apply_subst:subst -> clock_info -> clock_info
+
+(** Raises an error is the 2 clock_info are not unifiable *)
+val f : Lxm.t -> subst -> clock_info -> clock_info -> subst
+val list : Lxm.t -> clock_info list -> subst -> clock_info * subst
diff --git a/src/unify.ml b/src/unifyType.ml
similarity index 97%
rename from src/unify.ml
rename to src/unifyType.ml
index 5a71fd10..aa8708b2 100644
--- a/src/unify.ml
+++ b/src/unifyType.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 10:07) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/06/2008 (at 14:50) by Erwan Jahier> *)
open CompiledData
@@ -176,11 +176,8 @@ let unit_test () =
for i = 1 to 1000 do
let (tl1, tl2) = gen_unifiable_typeff_of_size (1+ Random.int 10) in
print_string (
- " ==> try Unify.proposition1 with lists " ^
+ " ==> try UnifyType.proposition1 with lists " ^
(CompiledDataDump.type_eff_list_to_string tl1) ^ " and " ^
(CompiledDataDump.type_eff_list_to_string tl2) ^ "\n");
assert (proposition1 tl1 tl2)
done
-
-
-
diff --git a/src/unify.mli b/src/unifyType.mli
similarity index 100%
rename from src/unify.mli
rename to src/unifyType.mli
diff --git a/src/uniqueOutput.ml b/src/uniqueOutput.ml
index e2adcb25..00c49ff1 100644
--- a/src/uniqueOutput.ml
+++ b/src/uniqueOutput.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 23/06/2008 (at 15:51) by Erwan Jahier> *)
+(** Time-stamp: <modified the 25/06/2008 (at 16:40) by Erwan Jahier> *)
open CompiledData
open Lxm
@@ -194,6 +194,16 @@ let (check : CompiledData.node_exp_eff -> Lxm.t -> unit) =
| BodyEff{ eqs_eff = eql } ->
let lel = List.flatten (List.map (fun {it=(left,_)} -> left) eql) in
let lel_map = partition_var lel in
+ (* Check that one does not define an input *)
+ VarMap.iter
+ (fun v _ ->
+ if v.var_nature_eff = SyntaxTreeCore.VarInput then
+ let msg = "\n*** Error; " ^(id2str v.var_name_eff) ^
+ " is an input, and thus cannot be defined."
+ in
+ raise (Compile_error(lxm, msg))
+ )
+ lel_map;
List.iter
(fun v ->
try check_one_var lxm v (VarMap.find v lel_map)
diff --git a/src/uniqueOutput.mli b/src/uniqueOutput.mli
index 5bbab223..f9a7d674 100644
--- a/src/uniqueOutput.mli
+++ b/src/uniqueOutput.mli
@@ -1,6 +1,6 @@
-(** Time-stamp: <modified the 23/06/2008 (at 15:48) by Erwan Jahier> *)
+(** Time-stamp: <modified the 25/06/2008 (at 16:34) by Erwan Jahier> *)
(** Check that each output and each local variable is defined at most
- and at least once. *)
+ and at least once. Also check that one does not try ti define an input. *)
val check : CompiledData.node_exp_eff -> Lxm.t -> unit
--
GitLab