From 7c49b4c2266a6e650c0953b2181495a1024e8c9a Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Mon, 30 Jun 2008 10:21:08 +0200
Subject: [PATCH] Check checking: add support for iterators.
---
src/predefEvalClock.ml | 23 +-
src/predefEvalType.ml | 5 +-
src/predefEvalType.mli | 8 +-
src/test/should_work/lionel/deSimone.lus | 2 +-
src/test/test.res.exp | 2478 ++++++++++++++++++++--
5 files changed, 2368 insertions(+), 148 deletions(-)
diff --git a/src/predefEvalClock.ml b/src/predefEvalClock.ml
index 9b92826f..d7db24c6 100644
--- a/src/predefEvalClock.ml
+++ b/src/predefEvalClock.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 30/06/2008 (at 09:33) by Erwan Jahier> *)
+(** Time-stamp: <modified the 30/06/2008 (at 10:14) by Erwan Jahier> *)
open Predef
open CompiledData
@@ -26,9 +26,24 @@ let if_clock_profile lxm sargs =
| _ -> assert false
-let fillred_clock_profile lxm sargs = assert false
-let map_clock_profile lxm sargs = assert false
-let boolred_clock_profile lxm sargs = assert false
+
+let rec fill x n = if n > 0 then (x::(fill x (n-1))) else []
+
+let fillred_clock_profile lxm sargs clks =
+ let (_, lto) = PredefEvalType.fillred_profile lxm sargs in
+ let clks = List.flatten clks in
+ fill (List.hd clks) (List.length lto)
+
+let map_clock_profile lxm sargs clks =
+ let (_, lto) = PredefEvalType.map_profile lxm sargs in
+ let clks = List.flatten clks in
+ fill (List.hd clks) (List.length lto)
+
+let boolred_clock_profile lxm sargs clks =
+ let (_, lto) = PredefEvalType.boolred_profile lxm sargs in
+ let clks = List.flatten clks in
+ fill (List.hd clks) (List.length lto)
+
(* This table contains the clock profile of predefined operators *)
let (f: op -> Lxm.t -> CompiledData.static_arg_eff list -> clocker) =
diff --git a/src/predefEvalType.ml b/src/predefEvalType.ml
index 022a4aff..8cb9690b 100644
--- a/src/predefEvalType.ml
+++ b/src/predefEvalType.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 26/06/2008 (at 14:49) by Erwan Jahier> *)
+(** Time-stamp: <modified the 30/06/2008 (at 09:49) by Erwan Jahier> *)
open Predef
open SyntaxTreeCore
@@ -99,7 +99,8 @@ let map_profile =
let get_id_type vi = vi.var_name_eff, vi.var_type_eff
-let fillred_profile =
+let (fillred_profile : Lxm.t -> CompiledData.static_arg_eff list ->
+ (Ident.t * type_eff) list * (Ident.t * type_eff) list) =
(* Given
- a node n of type tau * tau_1 * ... * tau_n -> tau * teta_1 * ... * teta_l
- a constant c (nb : sargs = [n,c])
diff --git a/src/predefEvalType.mli b/src/predefEvalType.mli
index 668759ba..eff63c3f 100644
--- a/src/predefEvalType.mli
+++ b/src/predefEvalType.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 09/06/2008 (at 12:23) by Erwan Jahier> *)
+(** Time-stamp: <modified the 30/06/2008 (at 09:50) by Erwan Jahier> *)
open CompiledData
@@ -20,3 +20,9 @@ val f : Predef.op -> Lxm.t -> CompiledData.static_arg_eff list -> typer
val make_node_exp_eff : Predef.op -> Lxm.t -> static_arg_eff list -> node_exp_eff
+val fillred_profile : Lxm.t -> CompiledData.static_arg_eff list ->
+ (Ident.t * type_eff) list * (Ident.t * type_eff) list
+val map_profile : Lxm.t -> CompiledData.static_arg_eff list ->
+ (Ident.t * type_eff) list * (Ident.t * type_eff) list
+val boolred_profile : Lxm.t -> CompiledData.static_arg_eff list ->
+ (Ident.t * type_eff) list * (Ident.t * type_eff) list
diff --git a/src/test/should_work/lionel/deSimone.lus b/src/test/should_work/lionel/deSimone.lus
index e859e9c9..e9c79e4b 100644
--- a/src/test/should_work/lionel/deSimone.lus
+++ b/src/test/should_work/lionel/deSimone.lus
@@ -48,7 +48,7 @@ node prop1(request : tabType) returns (ok : bool);
var acknowledge : tabType;
nb_acknowledge : int;
let
- acknowledge = deSimone(request);
+ acknowledge = deSimone(true, request);
nb_acknowledge = red<<prop1_iter;size>>(0,acknowledge);
ok = nb_acknowledge<=1;
tel
diff --git a/src/test/test.res.exp b/src/test/test.res.exp
index e2684be0..ddcfc412 100644
--- a/src/test/test.res.exp
+++ b/src/test/test.res.exp
@@ -28,9 +28,26 @@ let
co = (((ci and x) or (x and y)) or (y and ci));
tel
-- end of node Int8::fulladd
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/NONREG/Int.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/NONREG/PCOND.lus
@@ -1091,9 +1108,26 @@ extern node clock::all(
returns (
c:bool when b;
d:bool when c);
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 31, column 38
-*** when compiling lustre program should_work/NONREG/clock.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/NONREG/cminus.lus
@@ -3840,8 +3874,341 @@ let
tel
-- end of node Gyroscope2::TooFar
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/demo/Gyroscope2.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/alias.lus
@@ -3875,24 +4242,31 @@ let
o = Lustre::not(i);
tel
-- end of node alias::aliasPredefNot
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34
-*** when compiling lustre program should_work/demo/alias.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/bred.lus
Opening file /home/jahier/lus2lic/src/test/should_work/demo/bred.lus
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 31, column 38
-*** when compiling lustre program 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
----------------------------------------------------------------------
====> ../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;
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 31, column 38
-*** when compiling lustre program should_work/demo/bred_lv4.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/clock.lus
@@ -4126,9 +4500,30 @@ 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
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/demo/filliter.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/filter.lus
@@ -4244,8 +4639,21 @@ let
tel
-- end of node map_red_iter::traite_genCore_itere
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/demo/map_red_iter.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/mapdeRed.lus
@@ -4260,8 +4668,19 @@ let
tel
-- end of node mapdeRed::incr
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/demo/mapdeRed.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/mapiter.lus
@@ -4271,9 +4690,12 @@ let
b = (a + 1);
tel
-- end of node mapiter::incr_tab
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34
-*** when compiling lustre program should_work/demo/mapiter.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/mappredef.lus
@@ -4282,15 +4704,34 @@ const mappredef::N = 3;
type mappredef::tab_int = int^3;
type mappredef::tab_bool = bool^3;
-*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34
-*** when compiling lustre program should_work/demo/mappredef.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/plus.lus
Opening file /home/jahier/lus2lic/src/test/should_work/demo/plus.lus
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 31, column 38
-*** when compiling lustre program 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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/pre_x.lus
@@ -4309,9 +4750,11 @@ let
b = if ((init > a)) then (init) else (a);
tel
-- end of node rediter::max
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/demo/rediter.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/redoptest.lus
@@ -4321,9 +4764,11 @@ let
b = if ((init > a)) then (init) else (a);
tel
-- end of node redoptest::max
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/demo/redoptest.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/demo/sample_time_change.lus
@@ -4461,9 +4906,47 @@ 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
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/fab_test/iter.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/fab_test/iterate.lus
@@ -4481,8 +4964,70 @@ let
tel
-- end of node iterate::mapped
-*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34
-*** when compiling lustre program should_work/fab_test/iterate.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/fab_test/lecteur.lus
@@ -5965,8 +6510,19 @@ let
tel
-- end of node FillFollowedByRed::filled
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/FillFollowedByRed.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/Gyroscope.lus
@@ -6027,43 +6583,388 @@ let
tel
-- end of node Gyroscope::TooFar
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/Gyroscope.lus
-
-----------------------------------------------------------------------
-====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/ProduitBool/produitBool.lus
-Opening file /home/jahier/lus2lic/src/test/should_work/lionel/ProduitBool/produitBool.lus
-const produitBool::size = 10;
-type produitBool::Tacc_in = produitBool::Tacc_in {multiplieur : bool^10; rank : int};
-type produitBool::T_isElementOf_ = produitBool::T_isElementOf_ {eltToSearch : bool; iselementof : bool};
-type produitBool::iteratedStruct = produitBool::iteratedStruct {currentRank : int; rankToSelect : int; elementSelected : bool};
-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)
+node Gyroscope::assumeEvaluateAxis(
+ channels:Gyroscope::Faulty_ChannelT^4;
+ delta:real;
+ god:real;
+ delta_to_god:real)
returns (
- acc_out:produitBool::T_isElementOf_);
+ assumeOK:bool);
+var
+ NbToFar:int;
let
- acc_out =
- T_isElementOf_{eltToSearch=acc_in.eltToSearch;iselementof=(acc_in.iselementof
- or (acc_in.eltToSearch = elt_in))};
+ NbToFar = red<<node Gyroscope::TooFar, const 4>>(0, channels, god^4,
+ delta_to_god^4);
+ assumeOK = (NbToFar <= 1);
tel
--- end of node produitBool::iterated_isElementOf_
+-- end of node Gyroscope::assumeEvaluateAxis
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/ProduitBool/produitBool.lus
+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
-----------------------------------------------------------------------
-====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/ProduitBool/shiftFill_ludic.lus
-Opening file /home/jahier/lus2lic/src/test/should_work/lionel/ProduitBool/shiftFill_ludic.lus
-type shiftFill_ludic::T1_ARRAY = bool^10;
-type shiftFill_ludic::T4_STRUCT = shiftFill_ludic::T4_STRUCT {multiplieur : bool^10; rank : int};
-type shiftFill_ludic::T6_STRUCT = shiftFill_ludic::T6_STRUCT {eltToSearch : bool; iselementof : bool};
-type shiftFill_ludic::T5_STRUCT = shiftFill_ludic::T5_STRUCT {acc_in_PLC : shiftFill_ludic::T4_STRUCT; actual_rank : int};
-type shiftFill_ludic::t_Tacc_inShift = shiftFill_ludic::T5_STRUCT {acc_in_PLC : shiftFill_ludic::T4_STRUCT; actual_rank : int};
-type shiftFill_ludic::t_T_isElementOf_ = shiftFill_ludic::T6_STRUCT {eltToSearch : bool; iselementof : bool};
+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
+
+----------------------------------------------------------------------
+====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/ProduitBool/produitBool.lus
+Opening file /home/jahier/lus2lic/src/test/should_work/lionel/ProduitBool/produitBool.lus
+const produitBool::size = 10;
+type produitBool::Tacc_in = produitBool::Tacc_in {multiplieur : bool^10; rank : int};
+type produitBool::T_isElementOf_ = produitBool::T_isElementOf_ {eltToSearch : bool; iselementof : bool};
+type produitBool::iteratedStruct = produitBool::iteratedStruct {currentRank : int; rankToSelect : int; elementSelected : bool};
+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
+
+----------------------------------------------------------------------
+====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/ProduitBool/shiftFill_ludic.lus
+Opening file /home/jahier/lus2lic/src/test/should_work/lionel/ProduitBool/shiftFill_ludic.lus
+type shiftFill_ludic::T1_ARRAY = bool^10;
+type shiftFill_ludic::T4_STRUCT = shiftFill_ludic::T4_STRUCT {multiplieur : bool^10; rank : int};
+type shiftFill_ludic::T6_STRUCT = shiftFill_ludic::T6_STRUCT {eltToSearch : bool; iselementof : bool};
+type shiftFill_ludic::T5_STRUCT = shiftFill_ludic::T5_STRUCT {acc_in_PLC : shiftFill_ludic::T4_STRUCT; actual_rank : int};
+type shiftFill_ludic::t_Tacc_inShift = shiftFill_ludic::T5_STRUCT {acc_in_PLC : shiftFill_ludic::T4_STRUCT; actual_rank : int};
+type shiftFill_ludic::t_T_isElementOf_ = shiftFill_ludic::T6_STRUCT {eltToSearch : bool; iselementof : bool};
type shiftFill_ludic::T2_STRUCT = shiftFill_ludic::T2_STRUCT {multiplieur : bool^10; rank : int; actual_rank : int};
type shiftFill_ludic::t_Tacc_in = shiftFill_ludic::T4_STRUCT {multiplieur : bool^10; rank : int};
type shiftFill_ludic::t_Tacc_inShift2 = shiftFill_ludic::T2_STRUCT {multiplieur : bool^10; rank : int; actual_rank : int};
@@ -6084,8 +6985,36 @@ let
tel
-- end of node shiftFill_ludic::n_selectOneStage
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/ProduitBool/shiftFill_ludic.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/ProduitBool/shift_ludic.lus
@@ -6117,8 +7046,48 @@ let
tel
-- end of node shift_ludic::n_selectOneStage
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/ProduitBool/shift_ludic.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/arrays.lus
@@ -6136,9 +7105,77 @@ 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
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/arrays.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/calculs_max.lus
@@ -6178,9 +7215,17 @@ let
elt = ((s_in.icourant = s_in.imax1) or (s_in.icourant = s_in.imax2));
tel
-- end of node calculs_max::fill_bool
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/calculs_max.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/deSimone.lus
@@ -6213,8 +7258,29 @@ let
tel
-- end of node deSimone::prop1_iter
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/deSimone.lus
+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
+node deSimone::prop1(request:bool^10) returns (ok:bool);
+var
+ acknowledge:bool^10;
+ nb_acknowledge:int;
+let
+ acknowledge = deSimone::deSimone(true, request);
+ nb_acknowledge = red<<node deSimone::prop1_iter, const 10>>(0,
+ acknowledge);
+ ok = (nb_acknowledge <= 1);
+tel
+-- end of node deSimone::prop1
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/iterFibo.lus
@@ -6226,9 +7292,13 @@ let
elt = (accu_in[0] + accu_in[1]);
tel
-- end of node iterFibo::fibo
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/iterFibo.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/mapiter.lus
@@ -6258,9 +7328,40 @@ let
(sacc, out) = Lustre::fill<<node mapiter::bitalt, const 2>>(in);
tel
-- end of node mapiter::fill_bitalt
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/mapiter.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/matrice.lus
@@ -6274,27 +7375,57 @@ let
elt = (accu_in[0] + accu_in[1]);
tel
-- end of node matrice::fibo
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/matrice.lus
+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
----------------------------------------------------------------------
====> ../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;
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/matrice2.lus
+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
----------------------------------------------------------------------
====> ../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
-*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34
-*** when compiling lustre program should_work/lionel/minus.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/moyenne.lus
@@ -6312,9 +7443,15 @@ let
elt_in) / (accu_in.rank + 1.0));rank=(accu_in.rank + 1.0)};
tel
-- end of node moyenne::moyenne_step
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/moyenne.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/normal.lus
@@ -6348,8 +7485,306 @@ let
tel
-- end of node normal::int2InfoChgIndiv
-*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34
-*** when compiling lustre program should_work/lionel/normal.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/pipeline.lus
@@ -6367,33 +7802,124 @@ 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
+
+----------------------------------------------------------------------
+====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/predefOp.lus
+Opening file /home/jahier/lus2lic/src/test/should_work/lionel/predefOp.lus
+const predefOp::L = 2;
+type predefOp::Reg_L = bool^2;
+const predefOp::H = 3;
+type predefOp::T_Reg_H = bool^2^3;
+type predefOp::Tab_L = int^2;
+type predefOp::T_Tab_H = int^2^3;
+node predefOp::incr(init:int; b:bool) returns (res:int);
+let
+ res = if ((b = true)) then ((init + 1)) else (init);
+tel
+-- end of node predefOp::incr
+node predefOp::bitalt(iacc:bool) returns (oacc:bool; res:bool);
+let
+ res = iacc;
+ 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
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/pipeline.lus
+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
-----------------------------------------------------------------------
-====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/predefOp.lus
-Opening file /home/jahier/lus2lic/src/test/should_work/lionel/predefOp.lus
-const predefOp::L = 2;
-type predefOp::Reg_L = bool^2;
-const predefOp::H = 3;
-type predefOp::T_Reg_H = bool^2^3;
-type predefOp::Tab_L = int^2;
-type predefOp::T_Tab_H = int^2^3;
-node predefOp::incr(init:int; b:bool) returns (res:int);
+node predefOp::composematint(
+ i1:int^2^3;
+ i2:int^2^3)
+returns (
+ s1:int^2^3;
+ s2:bool^2^3);
let
- res = if ((b = true)) then ((init + 1)) else (init);
+ 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::incr
-node predefOp::bitalt(iacc:bool) returns (oacc:bool; res:bool);
+-- end of node predefOp::composematint
+node predefOp::incremental(iacc:int) returns (oacc:int; res:int);
let
res = iacc;
- oacc = not(res);
+ oacc = (res + 1);
tel
--- end of node predefOp::bitalt
+-- 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
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/predefOp.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/redIf.lus
@@ -6403,18 +7929,22 @@ let
r = if (a) then (b) else (c);
tel
-- end of node redIf::monIf
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/redIf.lus
+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
----------------------------------------------------------------------
====> ../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;
-
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/simpleRed.lus
+node simpleRed::simpleRed(a:int) returns (res:int);
+let
+ res = red<<node Lustre::+, const 3>>(0, a^3);
+tel
+-- end of node simpleRed::simpleRed
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/testSilus.lus
@@ -6450,8 +7980,254 @@ let
tel
-- end of node testSilus::int2InfoChgIndiv
-*** oops: an internal error occurred in file predefEvalClock.ml, line 30, column 34
-*** when compiling lustre program should_work/lionel/testSilus.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/lionel/triSel.lus
@@ -6481,8 +8257,89 @@ let
tel
-- end of node triSel::minFromRank
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/lionel/triSel.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/packEnvTest/Condact.lus
@@ -6530,8 +8387,21 @@ let
tel
-- end of node contractForElementSelectionInArray::selectOneStage
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/packEnvTest/contractForElementSelectionInArray/contractForElementSelectionInArray.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/packEnvTest/contractForElementSelectionInArray/main.lus
@@ -6568,9 +8438,255 @@ let
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_
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/packEnvTest/contractForElementSelectionInArray/main.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/packEnvTest/contractForElementSelectionInArray/noeudsIndependants.lus
@@ -6617,8 +8733,90 @@ let
tel
-- end of node tri::minFromRank
-*** oops: an internal error occurred in file predefEvalClock.ml, line 29, column 38
-*** when compiling lustre program should_work/packEnvTest/contractForElementSelectionInArray/tri.lus
+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
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/packEnvTest/modelInst.lus
--
GitLab