Made the Scade example compile

This commit is contained in:
Cédric Pasteur 2011-09-05 16:03:39 +02:00
parent 5843869adb
commit ace0cec555
5 changed files with 57 additions and 41 deletions

View file

@ -0,0 +1,29 @@
HEPTC=../../compiler/heptc.byte
HEPTC_OPTIONS=
VERBOSE=1
interfaces=(typeBase.epi typeTracks.epi typeArray.epi cstArrayInit.epi cstBaseInit.epi cstPhysics.epi cstTracksInit.epi mc_TypeInputs.epi mc_TypeLists.epi mc_TypeSensors.epi)
ext_libs=(mc_ext.epi mathext.epi)
sources=(math.ept trackslib.ept digital.ept mc.ept dv.ept verif.ept debug.ept)
for f in ${interfaces[@]}; do
if [ $VERBOSE ] ; then
echo "**** Compiling interface: $f *******"
fi
$HEPTC $f
done
for f in ${ext_libs[@]}; do
if [ $VERBOSE ] ; then
echo "**** Compiling external lib: $f *******"
fi
$HEPTC $f
done
for f in ${sources[@]}; do
if [ $VERBOSE ] ; then
echo "**** Compiling source file: $f *******"
fi
$HEPTC -target c $f
done

View file

@ -1,4 +1,5 @@
open TypeArray
open TypeTracks
open CstArrayInit
open Mc_TypeSensors
open Mc
@ -27,7 +28,7 @@ fun dv_tracknumberexist(missiontrack : TypeTracks.tmissiontrack;
var l36 : bool;
let
l36 =
fold dv_sametracknumber <<ksizemissiontracksarray>>(
fold<<ksizemissiontracksarray>> dv_sametracknumber(
missiontrack^ksizemissiontracksarray, missiontracks, false);
accout = accin or l36;
tel
@ -48,7 +49,7 @@ fun dv_proof2(ifftracks : TypeArray.tifftracksarray;
var l33 : bool;
let
l33 =
fold dv_detectedbyiff <<ksizemissiontracksarray>>(missiontracks, true);
fold<<ksizemissiontracksarray>> dv_detectedbyiff(missiontracks, true);
proof2 = Verif.implies(ifftracks = kinitifftrackarray, l33);
tel
@ -58,7 +59,7 @@ fun dv_proof3(missiontracks : TypeArray.tmissiontracksarray)
var l33 : bool;
let
l33 =
fold dv_tracknumberexist <<ksizemissiontracksarray>>(
fold<<ksizemissiontracksarray>> dv_tracknumberexist(
missiontracks, missiontracks^ksizemissiontracksarray, false);
proof3 = not l33;
tel

View file

@ -8,5 +8,5 @@ tel
-- and 0.0 if input is equal to 0.0 *)
fun sign(a : float) returns (o : float)
let
o = if a >. 0.0 then 1.0 else if 0.0 =. a then 0.0 else -. 1.0;
o = if a >. 0.0 then 1.0 else if 0.0 = a then 0.0 else -. 1.0;
tel

View file

@ -113,9 +113,9 @@ var
l30 : TypeTracks.trdrtrack^ksizerdrtracksarray;
let
rdrtracks = if st = TState_ON then l30 else kinitrdrtrackarray;
l30 = map Trackslib.elaboraterdrtrack <<ksizerdrtracksarray>>(l22);
l30 = map<<ksizerdrtracksarray>> Trackslib.elaboraterdrtrack(l22);
l22 =
map Trackslib.selectdetectedtrack <<ksizerdrtracksarray>>(
map<<ksizerdrtracksarray>> Trackslib.selectdetectedtrack(
rdrdetectedtracks, tracks^ksizerdrtracksarray,
CstTracksInit.kinittrack^ksizerdrtracksarray);
tel
@ -171,10 +171,10 @@ var l34 : TypeTracks.ttrack^TypeArray.ksizeifftracksarray;
l40 : TypeArray.tifftracksarray;
let
l34 =
map Trackslib.selectdetectedtrack <<ksizeifftracksarray>>(
map<<ksizeifftracksarray>> Trackslib.selectdetectedtrack(
iffdetectedtracks, tracks^ksizeifftracksarray,
CstTracksInit.kinittrack^ksizeifftracksarray);
l40 = map ifftrack_of_track <<ksizeifftracksarray>>(l34);
l40 = map<<ksizeifftracksarray>> ifftrack_of_track(l34);
ifftracks = if st = TState_ON then l40 else kinitifftrackarray;
tel
@ -250,10 +250,7 @@ tel
node createtracks_rand(res : bool)
returns (tracks : TypeArray.ttracksarray)
let
tracks =
map
createtracks_createonetrack_rand
<<ksizetracksarray>>(res^ksizetracksarray);
tracks = map<<ksizetracksarray>> createtracks_createonetrack_rand(res^ksizetracksarray);
tel
node createalltracks(res : bool)
@ -309,7 +306,7 @@ fun mc_tracks_fusion_onerdrwithifftracks(rdrtrack : TypeTracks.tmissiontrack;
fusionnedifftracks : TypeTracks.tmissiontrack^ksizeifftracksarray)
let
(fusionnedifftracks, fusionnedrdrtrack) =
mapfold fusionrdrifftracks <<ksizeifftracksarray>>(ifftracks, rdrtrack);
mapfold<<ksizeifftracksarray>> fusionrdrifftracks(ifftracks, rdrtrack);
tel
(* merge tracks data received from both radar and iff sensors *)
@ -324,16 +321,9 @@ var
let
missiontracks = mergedrdrtracks @ mergedifftracks;
(mergedrdrtracks, mergedifftracks) =
mapfold mc_tracks_fusion_onerdrwithifftracks <<ksizerdrtracksarray>>(
l140, l139);
l140 =
map
Trackslib.convertrdrtracktomissiontrack
<<ksizerdrtracksarray>>(rdrtracks);
l139 =
map
Trackslib.convertifftracktomissiontrack
<<ksizeifftracksarray>>(ifftracks);
mapfold<<ksizerdrtracksarray>> mc_tracks_fusion_onerdrwithifftracks(l140, l139);
l140 = map<<ksizerdrtracksarray>> Trackslib.convertrdrtracktomissiontrack(rdrtracks);
l139 = map<<ksizeifftracksarray>> Trackslib.convertifftracktomissiontrack(ifftracks);
tel
@ -358,7 +348,7 @@ let
not Trackslib.trackalowerprioritythanb(missiontrack,
accprioritymissiontrack);
missiontracknotinpriorittiesarray =
fold prio_tracknumbernotinarray <<4>>(missiontrack.m_tracknumber^4,
fold<<4>> prio_tracknumbernotinarray(missiontrack.m_tracknumber^4,
prioritiesarray, true);
prioritymissiontrack =
if missiontracknotinpriorittiesarray & missiontrackhashigherprioritythanacc
@ -379,9 +369,7 @@ let
[ prioritiesarray with [indexpriority] =
missiontrackwithhighestpriority.m_tracknumber ];
missiontrackwithhighestpriority =
fold
prio_selecthighestprioritynotinpriorityarray
<<ksizemissiontracksarray>>(
fold<<ksizemissiontracksarray>> prio_selecthighestprioritynotinpriorityarray(
missiontracks,
prioritiesarray^ksizemissiontracksarray, CstTracksInit.kinitmissiontrack);
tel
@ -402,7 +390,7 @@ fun prio_setpriorityinmissiontrackarray(priorityarray : Mc_TypeLists.tpriorityLi
returns (missiontrackwithprio : TypeTracks.tmissiontrack)
let
missiontrackwithprio =
foldi prio_setpriorityinmissiontrack <<4>>(priorityarray, missiontrack);
foldi<<4>> prio_setpriorityinmissiontrack(priorityarray, missiontrack);
tel
@ -426,7 +414,7 @@ node mc_tracks_prio(missiontracks : TypeArray.tmissiontracksarray)
var prioritytracknumbers : Mc_TypeLists.tpriorityList;
let
missiontrackswithprio =
map prio_setpriorityinmissiontrackarray <<ksizemissiontracksarray>>(
map<<ksizemissiontracksarray>> prio_setpriorityinmissiontrackarray(
prioritytracknumbers^ksizemissiontracksarray, missiontracks);
prioritytracknumbers =
prio_selectprioritarymissiontracks(missiontracks,
@ -442,10 +430,8 @@ node mc_tracks_tracknumber(withouttracknb : TypeArray.tmissiontracksarray)
var l81 : int;
let
(withtracknumber, l81) =
mapfold
Trackslib.calculatemissiontracknumber
<<ksizemissiontracksarray>>((kinitmissiontrackarray ->
pre withtracknumber)^ksizemissiontracksarray,
mapfold<<ksizemissiontracksarray>> Trackslib.calculatemissiontracknumber
((kinitmissiontrackarray -> pre withtracknumber)^ksizemissiontracksarray,
withouttracknb, 0 -> pre l81);
tel
@ -474,7 +460,7 @@ node mc(currentrdrstate : tsensorstate;
currentiffstate : tsensorstate;
ifftracks : TypeArray.tifftracksarray)
returns (rdronoffcmd, rdrmodecmd : bool;
missiontracks : Typearray.tmissiontracksarray;
missiontracks : TypeArray.tmissiontracksarray;
iffonoffcmd : bool)
let
missiontracks = mc_tracks(rdrtracks, ifftracks);

View file

@ -224,7 +224,7 @@ let
newtracknumber =
if setnewtracknumber then currenttracknumber + 1 else currenttracknumber;
previoustracknumber =
fold missiontrackexist <<TypeArray.ksizemissiontracksarray>>
fold <<TypeArray.ksizemissiontracksarray>> missiontrackexist
(missiontrack^TypeArray.ksizemissiontracksarray,
previousmissiontracks, 0);
newmissiontrack =
@ -239,7 +239,7 @@ fun calculatetracktargettypefromid(id : int)
let
targettype =
if 0 = id
then Typebase.Ttargettype_unknown
then TypeBase.Ttargettype_unknown
else if id <= 500
then TypeBase.Ttargettype_friend
else TypeBase.Ttargettype_foe;
@ -247,15 +247,15 @@ tel
(* calculate the derivative of a value x(n) according to its
ante-previous value x(n-2) *)
node myderivative(in, period : float) returns (out : float)
node myderivative(inv, period : float) returns (out : float)
var l2 : float;
let
(* l2 = fby (in; 2; 0.0); *)
l2 = 0.0 fby (0.0 fby in);
(* l2 = fby (inv; 2; 0.0); *)
l2 = 0.0 fby (0.0 fby inv);
out =
if Math.abs(l2) <. 0.1 or Math.abs(in) <. 0.1
if Math.abs(l2) <. 0.1 or Math.abs(inv) <. 0.1
then 0.0
else 0.0 -> (in -. l2) /. (2.0 *. period);
else 0.0 -> (inv -. l2) /. (2.0 *. period);
tel
(* calculate a track speed vector according to the position vector *)