diff --git a/.depend b/.depend
deleted file mode 100644
index 034efe0fc6f1b73888beb8395e3c8228862c07f1..0000000000000000000000000000000000000000
--- a/.depend
+++ /dev/null
@@ -1,119 +0,0 @@
-./obj-i386-linux-gcc3/compUtils.cmo: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/errors.cmx
-./obj-i386-linux-gcc3/compUtils.cmx: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmx ./obj-i386-linux-gcc3/errors.cmx
-./obj-i386-linux-gcc3/compile.cmo: ./obj-i386-linux-gcc3/verbose.cmi \
- ./obj-i386-linux-gcc3/syntaxe.cmx ./obj-i386-linux-gcc3/srcTab.cmi \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/lazyCompiler.cmi \
- ./obj-i386-linux-gcc3/errors.cmx ./obj-i386-linux-gcc3/compileData.cmx \
- ./obj-i386-linux-gcc3/compUtils.cmx
-./obj-i386-linux-gcc3/compile.cmx: ./obj-i386-linux-gcc3/verbose.cmx \
- ./obj-i386-linux-gcc3/syntaxe.cmx ./obj-i386-linux-gcc3/srcTab.cmx \
- ./obj-i386-linux-gcc3/lxm.cmx ./obj-i386-linux-gcc3/lazyCompiler.cmx \
- ./obj-i386-linux-gcc3/errors.cmx ./obj-i386-linux-gcc3/compileData.cmx \
- ./obj-i386-linux-gcc3/compUtils.cmx
-./obj-i386-linux-gcc3/compileData.cmo: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/errors.cmx \
- ./obj-i386-linux-gcc3/dump.cmx ./obj-i386-linux-gcc3/compUtils.cmx
-./obj-i386-linux-gcc3/compileData.cmx: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmx ./obj-i386-linux-gcc3/errors.cmx \
- ./obj-i386-linux-gcc3/dump.cmx ./obj-i386-linux-gcc3/compUtils.cmx
-./obj-i386-linux-gcc3/dump.cmo: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/errors.cmx
-./obj-i386-linux-gcc3/dump.cmx: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmx ./obj-i386-linux-gcc3/errors.cmx
-./obj-i386-linux-gcc3/errors.cmo: ./obj-i386-linux-gcc3/lxm.cmi
-./obj-i386-linux-gcc3/errors.cmx: ./obj-i386-linux-gcc3/lxm.cmx
-./obj-i386-linux-gcc3/evalConst.cmo: ./obj-i386-linux-gcc3/utils.cmx \
- ./obj-i386-linux-gcc3/syntaxe.cmx ./obj-i386-linux-gcc3/lxm.cmi \
- ./obj-i386-linux-gcc3/errors.cmx ./obj-i386-linux-gcc3/compileData.cmx \
- ./obj-i386-linux-gcc3/compUtils.cmx ./obj-i386-linux-gcc3/evalConst.cmi
-./obj-i386-linux-gcc3/evalConst.cmx: ./obj-i386-linux-gcc3/utils.cmx \
- ./obj-i386-linux-gcc3/syntaxe.cmx ./obj-i386-linux-gcc3/lxm.cmx \
- ./obj-i386-linux-gcc3/errors.cmx ./obj-i386-linux-gcc3/compileData.cmx \
- ./obj-i386-linux-gcc3/compUtils.cmx ./obj-i386-linux-gcc3/evalConst.cmi
-./obj-i386-linux-gcc3/evalType.cmo: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/evalConst.cmi \
- ./obj-i386-linux-gcc3/errors.cmx ./obj-i386-linux-gcc3/compileData.cmx \
- ./obj-i386-linux-gcc3/evalType.cmi
-./obj-i386-linux-gcc3/evalType.cmx: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmx ./obj-i386-linux-gcc3/evalConst.cmx \
- ./obj-i386-linux-gcc3/errors.cmx ./obj-i386-linux-gcc3/compileData.cmx \
- ./obj-i386-linux-gcc3/evalType.cmi
-./obj-i386-linux-gcc3/expandPack.cmo: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/errors.cmx \
- ./obj-i386-linux-gcc3/compUtils.cmx ./obj-i386-linux-gcc3/expandPack.cmi
-./obj-i386-linux-gcc3/expandPack.cmx: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmx ./obj-i386-linux-gcc3/errors.cmx \
- ./obj-i386-linux-gcc3/compUtils.cmx ./obj-i386-linux-gcc3/expandPack.cmi
-./obj-i386-linux-gcc3/lazyCompiler.cmo: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/symbolTab.cmi ./obj-i386-linux-gcc3/srcTab.cmi \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/evalType.cmi \
- ./obj-i386-linux-gcc3/evalConst.cmi ./obj-i386-linux-gcc3/errors.cmx \
- ./obj-i386-linux-gcc3/compileData.cmx ./obj-i386-linux-gcc3/compUtils.cmx \
- ./obj-i386-linux-gcc3/lazyCompiler.cmi
-./obj-i386-linux-gcc3/lazyCompiler.cmx: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/symbolTab.cmx ./obj-i386-linux-gcc3/srcTab.cmx \
- ./obj-i386-linux-gcc3/lxm.cmx ./obj-i386-linux-gcc3/evalType.cmx \
- ./obj-i386-linux-gcc3/evalConst.cmx ./obj-i386-linux-gcc3/errors.cmx \
- ./obj-i386-linux-gcc3/compileData.cmx ./obj-i386-linux-gcc3/compUtils.cmx \
- ./obj-i386-linux-gcc3/lazyCompiler.cmi
-./obj-i386-linux-gcc3/lexer.cmo: ./obj-i386-linux-gcc3/parser.cmi \
- ./obj-i386-linux-gcc3/lxm.cmi
-./obj-i386-linux-gcc3/lexer.cmx: ./obj-i386-linux-gcc3/parser.cmx \
- ./obj-i386-linux-gcc3/lxm.cmx
-./obj-i386-linux-gcc3/lxm.cmo: ./obj-i386-linux-gcc3/lxm.cmi
-./obj-i386-linux-gcc3/lxm.cmx: ./obj-i386-linux-gcc3/lxm.cmi
-./obj-i386-linux-gcc3/main.cmo: ./obj-i386-linux-gcc3/version.cmx \
- ./obj-i386-linux-gcc3/verbose.cmi ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/parser.cmi ./obj-i386-linux-gcc3/lxm.cmi \
- ./obj-i386-linux-gcc3/lexer.cmx ./obj-i386-linux-gcc3/errors.cmx \
- ./obj-i386-linux-gcc3/dump.cmx ./obj-i386-linux-gcc3/compile.cmx
-./obj-i386-linux-gcc3/main.cmx: ./obj-i386-linux-gcc3/version.cmx \
- ./obj-i386-linux-gcc3/verbose.cmx ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/parser.cmx ./obj-i386-linux-gcc3/lxm.cmx \
- ./obj-i386-linux-gcc3/lexer.cmx ./obj-i386-linux-gcc3/errors.cmx \
- ./obj-i386-linux-gcc3/dump.cmx ./obj-i386-linux-gcc3/compile.cmx
-./obj-i386-linux-gcc3/parser.cmo: ./obj-i386-linux-gcc3/utils.cmx \
- ./obj-i386-linux-gcc3/syntaxe.cmx ./obj-i386-linux-gcc3/lxm.cmi \
- ./obj-i386-linux-gcc3/errors.cmx ./obj-i386-linux-gcc3/parser.cmi
-./obj-i386-linux-gcc3/parser.cmx: ./obj-i386-linux-gcc3/utils.cmx \
- ./obj-i386-linux-gcc3/syntaxe.cmx ./obj-i386-linux-gcc3/lxm.cmx \
- ./obj-i386-linux-gcc3/errors.cmx ./obj-i386-linux-gcc3/parser.cmi
-./obj-i386-linux-gcc3/srcTab.cmo: ./obj-i386-linux-gcc3/verbose.cmi \
- ./obj-i386-linux-gcc3/syntaxe.cmx ./obj-i386-linux-gcc3/symbolTab.cmi \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/expandPack.cmi \
- ./obj-i386-linux-gcc3/errors.cmx ./obj-i386-linux-gcc3/compUtils.cmx \
- ./obj-i386-linux-gcc3/srcTab.cmi
-./obj-i386-linux-gcc3/srcTab.cmx: ./obj-i386-linux-gcc3/verbose.cmx \
- ./obj-i386-linux-gcc3/syntaxe.cmx ./obj-i386-linux-gcc3/symbolTab.cmx \
- ./obj-i386-linux-gcc3/lxm.cmx ./obj-i386-linux-gcc3/expandPack.cmx \
- ./obj-i386-linux-gcc3/errors.cmx ./obj-i386-linux-gcc3/compUtils.cmx \
- ./obj-i386-linux-gcc3/srcTab.cmi
-./obj-i386-linux-gcc3/symbolTab.cmo: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/errors.cmx \
- ./obj-i386-linux-gcc3/compUtils.cmx ./obj-i386-linux-gcc3/symbolTab.cmi
-./obj-i386-linux-gcc3/symbolTab.cmx: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmx ./obj-i386-linux-gcc3/errors.cmx \
- ./obj-i386-linux-gcc3/compUtils.cmx ./obj-i386-linux-gcc3/symbolTab.cmi
-./obj-i386-linux-gcc3/syntaxe.cmo: ./obj-i386-linux-gcc3/lxm.cmi \
- ./obj-i386-linux-gcc3/errors.cmx
-./obj-i386-linux-gcc3/syntaxe.cmx: ./obj-i386-linux-gcc3/lxm.cmx \
- ./obj-i386-linux-gcc3/errors.cmx
-./obj-i386-linux-gcc3/verbose.cmo: ./obj-i386-linux-gcc3/verbose.cmi
-./obj-i386-linux-gcc3/verbose.cmx: ./obj-i386-linux-gcc3/verbose.cmi
-./obj-i386-linux-gcc3/evalConst.cmi: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/compileData.cmx
-./obj-i386-linux-gcc3/evalType.cmi: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/compileData.cmx
-./obj-i386-linux-gcc3/expandPack.cmi: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmi
-./obj-i386-linux-gcc3/lazyCompiler.cmi: ./obj-i386-linux-gcc3/srcTab.cmi \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/compileData.cmx \
- ./obj-i386-linux-gcc3/compUtils.cmx
-./obj-i386-linux-gcc3/parser.cmi: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmi
-./obj-i386-linux-gcc3/srcTab.cmi: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/symbolTab.cmi
-./obj-i386-linux-gcc3/symbolTab.cmi: ./obj-i386-linux-gcc3/syntaxe.cmx \
- ./obj-i386-linux-gcc3/lxm.cmi ./obj-i386-linux-gcc3/compUtils.cmx
diff --git a/AUTHORS.txt b/AUTHORS.txt
index bebb221bf9fb61f0d3534cfbc5963125abfcba17..c9f93bcc312aab4b3699157c1e8cd4a94884b0b3 100644
--- a/AUTHORS.txt
+++ b/AUTHORS.txt
@@ -1,5 +1,5 @@
(* OASIS_START *)
-(* DO NOT EDIT (digest: ad71f10e8bf85f1525b15846752a46b9) *)
+(* DO NOT EDIT (digest: e0c07255abb5e78e10ac950c68a2b7d7) *)
Authors of lustre-v6:
@@ -7,6 +7,6 @@ Authors of lustre-v6:
Current maintainers of lustre-v6:
-* erwan.jahier@imag.fr
+* erwan.jahier@univ-grenoble-alpes.fr
(* OASIS_STOP *)
diff --git a/Makefile b/Makefile
index cc9f14579bffafd1b816e96d184a4a3f30366b54..a57615b29e4d2a53ec280da8c307cd2b2c429df8 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,5 @@
-all:build
+all:build
build: setup.data src/lv6version.ml
ocaml setup.ml -build
diff --git a/Makefile.dev b/Makefile.dev
index b327a5af803f4ac852df678845b633581e6b67e7..5c3f58073f5996482478e2947dc1ba2e9f673884 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -23,6 +23,12 @@ qtest:
cd $(TESTDIR) ; make test ; make time
cd $(curdir)
+#######################################################################################
+#
+
+README.md: README.txt
+ cat $< | grep -v "^(\*" > $@
+
#######################################################################################
# git entry points
@@ -62,15 +68,6 @@ ci:
amend:
test -f committed && git commit -a -F log --amend
-###############################
-# forge
-
-push:
- git push git+ssh://$(USER)@scm.forge.imag.fr/var/lib/gforge/chroot/scmrepos/git/lustre/lus2lic.git
-
-pull:
- git pull git+ssh://$(USER)@scm.forge.imag.fr/var/lib/gforge/chroot/scmrepos/git/lustre/lus2lic.git
-
###############################
# opam-ing
@@ -106,13 +103,7 @@ opam-test : $(WWWTEST)/pool/$(PACKNAME).tgz
oasis2opam $(HTTPTEST)/pool/$(PACKNAME).tgz && \
cd .. ; opam-admin check && opam-admin make -g
-verimag:
- echo "su synchron + opam update + opam upgrade "
-#
-# nb : pour installer la derniere version dans /usr/local/tools/lustre/v6
-# il suffit de faire
-# make opam + su synchron + opam update + opam upgrade
###############################
# install pre-compiled binaries
@@ -163,13 +154,3 @@ www-dist:dist
cp $(TGZ) $(WWW)/lustre-v6/pre-compiled/
-###############################
-# tags
-
-OTAGS=~/.opam/4.02.1+PIC/bin/otags
-# otags don't manage to parse gnuplotRif.ml
-NO_TAGS=gnuplotRif.ml
-tags:
- $(OTAGS) -v $(shell ocamlc -where)/*.mli $(shell ls src/*.ml | grep -v $(NO_TAGS))
-tags2:
- $(OTAGS) -v $(shell ls src/*.ml | grep -v $(NO_TAGS))
diff --git a/README.md b/README.md
index 50acdeb5bdc3334d7e162038eac334c4c3a2ff5e..fdb1066367b09a057bf07170b6176a916402bb1d 100644
--- a/README.md
+++ b/README.md
@@ -1,12 +1,11 @@
-(* OASIS_START *)
-(* DO NOT EDIT (digest: 7018be8ddc148ce8fff24df3fef8d341) *)
lustre-v6 - The Lustre V6 Verimag compiler
==========================================
-This package contains: (1) lus2lic: the (current) name of the compiler (and
-interpreter via -exec). (2) the lustre-v6 ocaml lib: allows to call the
-Lustre v6 interpreter ocaml
+This package contains:\n - lus2lic: the (current) name of the compiler (and
+interpreter via -exec) - the lustre-v6 ocaml lib: allows to call the Lustre
+v6 interpreter ocaml - the lustre-v6 rdbg plugin: allows to debug Lustre v6
+program wth rdbg
See the file [INSTALL.txt](INSTALL.txt) for building and installation
instructions.
@@ -19,4 +18,3 @@ Copyright and license
lustre-v6 is distributed under the terms of the Proprietary license, all
rights reserved.
-(* OASIS_STOP *)
diff --git a/README.txt b/README.txt
index 50acdeb5bdc3334d7e162038eac334c4c3a2ff5e..e88a36b4dfe6d0065aad55768c4b6a8289bb3700 100644
--- a/README.txt
+++ b/README.txt
@@ -1,12 +1,13 @@
(* OASIS_START *)
-(* DO NOT EDIT (digest: 7018be8ddc148ce8fff24df3fef8d341) *)
+(* DO NOT EDIT (digest: 8ce36f72587bcf63a786f3ea98fd2fac) *)
lustre-v6 - The Lustre V6 Verimag compiler
==========================================
-This package contains: (1) lus2lic: the (current) name of the compiler (and
-interpreter via -exec). (2) the lustre-v6 ocaml lib: allows to call the
-Lustre v6 interpreter ocaml
+This package contains:\n - lus2lic: the (current) name of the compiler (and
+interpreter via -exec) - the lustre-v6 ocaml lib: allows to call the Lustre
+v6 interpreter ocaml - the lustre-v6 rdbg plugin: allows to debug Lustre v6
+program wth rdbg
See the file [INSTALL.txt](INSTALL.txt) for building and installation
instructions.
diff --git a/_oasis b/_oasis
index 497afcec10144282065ed0115402015f3eab3669..561091ebde1a60b9051e1c6324e845843f040e26 100644
--- a/_oasis
+++ b/_oasis
@@ -1,12 +1,13 @@
OASISFormat: 0.4
Name: lustre-v6
-Version: 1.720
+Version: 1.725
Synopsis: The Lustre V6 Verimag compiler
Description: This package contains:
- (1) lus2lic: the (current) name of the compiler (and interpreter via -exec).
- (2) the lustre-v6 ocaml lib: allows to call the Lustre v6 interpreter ocaml
+ - lus2lic: the (current) name of the compiler (and interpreter via -exec)
+ - the lustre-v6 ocaml lib: allows to call the Lustre v6 interpreter from ocaml
+ - the lustre-v6 rdbg plugin: allows to debug Lustre v6 program wth rdbg
Authors: Erwan Jahier and Pascal Raymond
-Maintainers: erwan.jahier@imag.fr
+Maintainers: erwan.jahier@univ-grenoble-alpes.fr
License: PROP
Plugins: DevFiles (0.3), META (0.3), StdFiles (0.3)
OCamlVersion: >= 4.02
diff --git a/_tags b/_tags
index 31d10a1ceb7033b9bd2dcd2bf40e7e77617b4173..15090ec4bc233807cb7c02cb79e3267f0fb8b1bb 100644
--- a/_tags
+++ b/_tags
@@ -35,4 +35,3 @@ true: annot, bin_annot
<src/*.ml{,i,y}>: package(str)
<src/*.ml{,i,y}>: package(unix)
# OASIS_STOP
-
diff --git a/lus2lic b/lus2lic
deleted file mode 120000
index d49b1adf51c76e1ce44da7eda487fae545182ce3..0000000000000000000000000000000000000000
--- a/lus2lic
+++ /dev/null
@@ -1 +0,0 @@
-main.native
\ No newline at end of file
diff --git a/notes.org b/readme-dev.org
similarity index 100%
rename from notes.org
rename to readme-dev.org
diff --git a/src/lv6version.ml b/src/lv6version.ml
index 669e7ab147d9f4d12a7ef2cf0c1a0f819d4f24a5..c83fce409fc25efc305c68bc98d0e5c38d024e94 100644
--- a/src/lv6version.ml
+++ b/src/lv6version.ml
@@ -1,7 +1,7 @@
(** Automatically generated from Makefile *)
let tool = "lus2lic"
let branch = "master"
-let commit = "720"
-let sha_1 = "a35d8a9a255bf2c97e3c200e720670829d2d585a"
+let commit = "725"
+let sha_1 = "e2a7250e8a41026e9366e342579f0607dfb5d068"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "erwan.jahier@univ-grenoble-alpes.fr"
diff --git a/tests-pascal/_test-old/Condact.lus b/tests-pascal/_test-old/Condact.lus
deleted file mode 100644
index 80d16fd046a69e6d33eba6749c459f5f4d0b237a..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/Condact.lus
+++ /dev/null
@@ -1,40 +0,0 @@
-(***********************************************
--- File: Condact.lus
--- Author: Yussef
--- Date: 19/03/2004
-***********************************************)
-
---------------------------------------
--- Generic Package Condact
--------------------------------------
-
-package Main
- provides node carre(e: int) returns (s: int);
-body
- node carre(e: int) returns (s: int);
- let
- s = e*e;
- tel
-end
-
-
-package TestCondact
---uses Main;
- is Condact(int,int,Main::carre);
-
-
-model Condact
- needs
- type t1;
- type t2;
- node n(x: t1) returns (y: t2);
-
- provides node C(c: bool; d: t2; x: t1) returns (y: t2);
-
-body
- node C(c: bool; d: t2; x: t1) returns (y: t2);
- let
- y = if c then current(n(x))
- else d -> pre y;
- tel
-end
diff --git a/tests-pascal/_test-old/Makefile b/tests-pascal/_test-old/Makefile
deleted file mode 100644
index 63b2819dcb5387be60c6759125abbad6921e6b1f..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/Makefile
+++ /dev/null
@@ -1,19 +0,0 @@
-
-LV6=../src/lus2lic
-
-test:
- rm -f test.res
- $(LV6) packages.lus -main mainPack:preced > test.res
- $(LV6) modelInst.lus -main main:main >> test.res
- $(LV6) Condact.lus -main TestCondact:C >> test.res
- diff -u test.res test.exp > test.diff
-
-diff:
- rm -f test.diff && diff -u test.res test.exp > test.diff || true
-
-
-update:
- cp test.res test.exp
-
-clean:
- rm -f *.xec *~
diff --git a/tests-pascal/_test-old/contractForElementSelectionInArray/contractForElementSelectionInArray.lus b/tests-pascal/_test-old/contractForElementSelectionInArray/contractForElementSelectionInArray.lus
deleted file mode 100644
index 28ec246896213ca04f00d85e3fbd8a82b5bb997e..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/contractForElementSelectionInArray/contractForElementSelectionInArray.lus
+++ /dev/null
@@ -1,22 +0,0 @@
-const size=10;
-
-type elementType = int;
-type iteratedStruct = {currentRank : int; rankToSelect : int; elementSelected : elementType};
-
-node selectEltInArray(array : elementType^size; rankToSelect : int) returns (elementSelected : elementType);
-var iterationResult : iteratedStruct;
-let
- iterationResult = red<<selectOneStage;size>>({0, rankToSelect, 0}, array);
- elementSelected = iterationResult.elementSelected;
-tel
-
-
-
-node selectOneStage(acc_in : elementType; currentElt : elementType) returns (acc_out : elementType);
-let
- acc_out = {currentRank = acc_in.currentRank+1;
- rankToSelect = acc_in.rankToSelect;
- elementSelected = if(acc_in.currentRank=acc_in.rankToSelect)
- then currentElt
- else acc_in.elementSelected};
-tel
diff --git a/tests-pascal/_test-old/contractForElementSelectionInArray/main.lus b/tests-pascal/_test-old/contractForElementSelectionInArray/main.lus
deleted file mode 100644
index 7f12a4d48d6750cd8bdafc066826441cec041b49..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/contractForElementSelectionInArray/main.lus
+++ /dev/null
@@ -1,28 +0,0 @@
---package intArray is packageTableau(int, 10, equals, gt);
---package intArray is packageTableau(int, 10, Lustre::eq, Lustre::igt);
-package intArray is packageTableau(int, 10, =, >);
---package intArray is packageTableau(int, 10, =, Lustre::igt);
-
---package Lustre is packageTableau(int, 10, =, >);
-
-package main
- uses intArray;--, intArray2, intArray3;
- provides node main(a : int^10) returns (tri : int^10; pos_min, min, pos_max, max: int);
-
-body
-
-node main(a : int^10) returns ( tri : int^10;
- pos_min,
- min,
- pos_max,
- 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
diff --git a/tests-pascal/_test-old/contractForElementSelectionInArray/noeudsIndependants.lus b/tests-pascal/_test-old/contractForElementSelectionInArray/noeudsIndependants.lus
deleted file mode 100644
index f188865c21e8996205b782a64a830c26f6832d93..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/contractForElementSelectionInArray/noeudsIndependants.lus
+++ /dev/null
@@ -1,10 +0,0 @@
-
-node equals(a, b : int) returns (r : bool);
-let
- r = a = b;
-tel
-
-node gt(a, b : int) returns (r : bool);
-let
- r = a > b;
-tel
diff --git a/tests-pascal/_test-old/contractForElementSelectionInArray/packageTableau.lus b/tests-pascal/_test-old/contractForElementSelectionInArray/packageTableau.lus
deleted file mode 100644
index 06f20ab6b21b4188906a6f9fad3900ba089ff44e..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/contractForElementSelectionInArray/packageTableau.lus
+++ /dev/null
@@ -1,375 +0,0 @@
-model packageTableau
-needs
- type elementType;
- const size : int; -- on doit supposer que size>0;
- node _isEqualTo_(e1 : elementType; e2 : elementType) returns (isequalto : bool);
- node _isGreaterThan_(e1 : elementType; e2 : elementType) returns (isgreaterthan : bool);
-
-provides
- type arrayType;
- node selectElementOfRank_inArray_(rankToSelect : int;array : arrayType) returns (elementSelected : elementType);
- node getMaximumIn_(array : arrayType) returns (maximumElement : elementType);
- node getRank_ofMaximumIn_(array : arrayType) returns (rankOfMaximumElement : int);
- node getMinimumIn_(array : arrayType) returns (minimumElement : elementType);
- node getRank_ofMinimumIn_(array : arrayType) returns (rankOfMinimumElement : int);
- node _isLoselySorted(array : arrayType) returns (array_isLoselySorted : bool);
- node sort_(array : arrayType) returns (arraySorted : arrayType);
- node _isElementOf_(e : elementType; t : arrayType) returns (iselementof : bool);
--- on peut encore imaginer:
--- 1) echange de 2 éléments dans un tableau (donnés par leurs indices)
--- 2) interclassement de 2 tableaux
-
---node interleaving(array1 : arrayType; array2 : arrayType) returns (interleavedArray : elementType^(2*size));
-
--- pour tester: on choisit un elementType facile: les entiers.
---const size = 10;
---type elementType = int;
-
---node _isEqualTo_(e1 : elementType; e2 : elementType) returns (isequalto : bool);
---let
--- isequalto = e1 = e2;
---tel
-
---node _isGreaterThan_(e1, e2 : elementType) returns (isgreaterthan : bool);
---let
--- isgreaterthan = e1>e2;
---tel
-
-
---node _isGreaterOrEqualTo_(e1, e2 : elementType) returns (ge : bool);
---let
--- ge = _isGreaterThan_(e1, e2) or _isEqualTo_(e1, e2);
---tel
-
-
-
-
-body
-
--- Type fourni: le type "tableau d'éléments elementType"
-type arrayType = elementType^size;
-
-
--- constantes et types internes
-type iteratedStruct = {currentRank : int; rankToSelect : int; elementSelected : elementType};
--- les types suivants sont uniquement utilisés pour l'algorithme de tri
-type Sort_accu = {CurrentRank : int,
- Tab : arrayType};
-type Exchange_accu = {MinVal : elementType,
- MinRank : int,
- RankFrom : int,
- CurrentVal : elementType,
- Rank : int};
-
-type Select_accu = {RankToFind : int,
- CurrentRank : int,
- Val : elementType};
-
-type MinFR_accu = {MinVal : elementType,
- MinRank : int,
- RankFrom : int,
- Rank : int};
-
-
--- est-ce qu'un element est dans un tableau
-type T_isElementOf_ = {eltToSearch : elementType, iselementof : bool};
-
-node _isElementOf_(e : elementType; t : arrayType) returns (iselementof : bool);
-var acc_out : T_isElementOf_;
-let
- acc_out = red<<iterated_isElementOf_;size>>({eltToSearch = e, iselementof = false}, t);
-tel
-
-
-node iterated_isElementOf_(acc_in : T_isElementOf_; elt_in : elementType) returns (acc_out : T_isElementOf_);
-let
- acc_out = {eltToSearch = acc_in.eltToSearch;
- iselementof = acc_in or _isEqualTo_(acc_in.eltToSearch, elt_in)};
-tel
-
-
-
--- noeud de selection d'un element dans un tableau
--- assume : rankToSelect>=0
--- guarantee : _isElementOf_(elementSelected, array);
-node selectElementOfRank_inArray_(rankToSelect : int;array : arrayType) returns (elementSelected : elementType)
-%ASSUME:assumeSelectElementOfRank_inArray_%
-%GUARANTEE:guaranteeSelectElementOfRank_inArray_%
-var iterationResult : iteratedStruct;
-let
- iterationResult = red<<selectOneStage;size>>({currentRank = 0, rankToSelect = rankToSelect, elementSelected = array[0]}, array);
- elementSelected = iterationResult.elementSelected;
-tel
-
-node assumeSelectElementOfRank_inArray_(rankToSelect : int;array : arrayType) returns (assumeOK : bool);
-let
- assumeOK = rankToSelect >= 0;
-tel
-
-node guaranteeSelectElementOfRank_inArray_(rankToSelect : int;array : arrayType; elementSelected : elementType) returns (guaranteeOK : bool);
-let
- guaranteeOK = _isElementOf_(elementSelected, array);
-tel
-
-
--- assume : acc_in.currentRank>=0
--- guarantee : acc_out.currentRank>acc_in.currentRank
-node selectOneStage(acc_in : iteratedStruct; currentElt : elementType) returns (acc_out : iteratedStruct);
-let
- acc_out = {currentRank = acc_in.currentRank+1;
- rankToSelect = acc_in.rankToSelect;
- elementSelected = if(acc_in.currentRank=acc_in.rankToSelect)
- then currentElt
- else acc_in.elementSelected};
-tel
-
---node assumeSelectOneStage(
-
-
-
-
--- determination du maximum
--- guarantee : forall<<_isGreaterOrEqualTo_;size>>(maximumElement^size, array);
-node getMaximumIn_(array : arrayType) returns (maximumElement : elementType);
-let
- maximumElement = red<<selectMax;size>>(array[0], array);
-tel
-
--- guarantee : _isGreaterOrEqualTo_(e, e1) or _isGreaterOrEqualTo_(e, e2)
-node selectMax(e1, e2 : elementType) returns (e : elementType);
-let
- e = if(_isGreaterThan_(e1, e2)) then e1 else e2;
-tel
-
-
-
--- determination du rang du maximum
-node getRank_ofMaximumIn_(array : arrayType) returns (rankOfMaximumElement : int);
-var local : currentRank_withMemorizedRank;
-let
- local = red<<selectMaxRank;size>>({currentRank = 0; rankOfMemorizedVal = 0; memorizedVal = array[0]}, array);
- rankOfMaximumElement = local.rankOfMemorizedVal;
-tel
-
-type currentRank_withMemorizedRank = {currentRank : int; rankOfMemorizedVal : int; memorizedVal : elementType};
-
-
-
--- assume : acc_in.currentRank>=0
--- guarantee : acc_out.currentRank>acc_in.currentRank
-node selectMaxRank(acc_in : currentRank_withMemorizedRank; e1 : elementType) returns (acc_out : currentRank_withMemorizedRank);
-let
- acc_out = {currentRank = acc_in.currentRank+1;
- rankOfMemorizedVal = if(_isGreaterThan_(e1, acc_in.memorizedVal)) then acc_in.currentRank else acc_in.rankOfMemorizedVal;
- memorizedVal = if(_isGreaterThan_(e1, acc_in.memorizedVal)) then e1 else acc_in.memorizedVal};
-tel
-
-
-
-
--- determination du minimum
--- guarantee : forall<<_isGreaterOrEqualTo_;size>>(array, minimumElement^size);
-node getMinimumIn_(array : arrayType) returns (minimumElement : elementType);
-var maximum : elementType;
-let
- maximum = getMaximumIn_(array);
- minimumElement = red<<selectMin;size>>(maximum, array);
-tel
-
-
-node selectMin(e1, e2 : elementType) returns (e : elementType);
-let
- e = if(_isGreaterThan_(e1, e2)) then e2 else e1;
-tel
-
-
--- determination du rang du minimum
--- guarantee rankOfMaximumElement>=0;
-node getRank_ofMinimumIn_(array : arrayType) returns (rankOfMinimumElement : int);
-var minElement : elementType;
-let
- minElement = getMinimumIn_(array);
- rankOfMinimumElement = red<<selectMinRank;size>>({currentRank = 0; rankOfMemorizedVal = 0; memorizedVal = minElement}, array).rankOfMemorizedVal;
-tel
-
-
--- assume : acc_in.currentRank>=0
--- guarantee : acc_out.currentRank>acc_in.currentRank
-node selectMinRank(acc_in : currentRank_withMemorizedRank; elt : elementType) returns (acc_out : currentRank_withMemorizedRank);
-let
- acc_out = {currentRank = acc_in.currentRank+1;
- rankOfMemorizedVal = if(_isEqualTo_(acc_in.memorizedVal, elt)) then acc_in.currentRank else acc_in.rankOfMemorizedVal;
- memorizedVal = acc_in.memorizedVal};
-tel
-
-
-type forSortingAlgo = {previousElement : elementType; sortedUpToHere : bool};
-
--- est-ce que le tableau est ordonné ?
-node _isLoselySorted(array : arrayType) returns (array_isLoselySorted : bool);
-var result : forSortingAlgo;
-let
- result = red<<isLocallyLoselySorted;size>>({previousElement = array[0]; sortedUpToHere = true}, array);
- array_isLoselySorted = result.sortedUpToHere;
-tel
-
-node isLocallyLoselySorted(acc_in : forSortingAlgo; elt : elementType) returns (acc_out : forSortingAlgo);
-let
- acc_out = {previousElement = elt;
- sortedUpToHere = _isGreaterOrEqualTo_(elt, acc_in.previousElement) and acc_in.sortedUpToHere};
-tel
-
-
-
--- Tri d'un tableau
--- guarantee : _isLoselySorted(arraySorted);
-node sort_(array : arrayType) returns (arraySorted : arrayType);
-var
- UnarySort_accu_out : Sort_accu;
-let
- UnarySort_accu_out = red<<UnarySort;size>>(
- {CurrentRank = 0,
- Tab = array}, -- Values given for test
- array); -- same
- arraySorted = UnarySort_accu_out.Tab;
-tel
-
-
-
-
--- Unary_sort takes as input an array of integers (accu_in.Tab).
--- First, it determines the minimum of the elements that are after the rank 'accu_in.currentRank'
--- in accu_in.Tab (it gets its rank and value)
--- Then it gets the current element of Tab (determinex by accu_in.currentRank) :
--- 'select' iteration
--- and switches it with the next minimum 'Exchange' iteration
--- accu_in.CurrentRank : indice permettant d'identifier les élements
--- traités jusque là. A cet étage de l'itération, on trie les élements
--- d'indice compris entre accu_in.CurrentRank et la taille du tableau -1
--- accu_in.Tab : tableau en cours de tri, Tab est tel que \forall i, j < accu_in.CurrentRank. i<j => Tab[i]<Tab[j]
--- accu_out.CurrentRank : accu_in.CurrentRank + 1 : à l'étage suivant de l'itération, on s'occupera de trier
--- les élements d'incide compris entre accu_out.CurrentRank et la taille du tableau -1
--- accu_in.Tab : tableau en cours de tri, Tab est tel que \forall i, j < accu_out.CurrentRank. i<j => Tab[i]<Tab[j]
-node UnarySort(accu_in : Sort_accu ; eltIn : int)
- returns (accu_out : Sort_accu);
-var
- accu_out_select : Select_accu;
--- accu_out_select.RankToFind : rang de l'élement dont on cherche la valeur
--- accu_out_select.CurrentRank : rang courant dans l'itération
--- accu_out_select.Val : valeur de l'élement de rang RankToFind
- accu_out_min : MinFR_accu;
--- accu_out_min.MinVal : valeur du minimum
--- accu_out_min.MinRank : rang du minimum
--- acc_out_min.RankFrom : rang à partir duquel on cherche le minimum
--- accu_out_min.Rank : rang courant (inutile en dehors de l'itération
- accu_out_exchange : Exchange_accu;
--- accu_out_exchange.MinVal : Valeur du minimum dans la tranche considérée
--- accu_out_exchange.MinRank : rang du minimum dans la tranche considérée
--- accu_out_exchange.RankFrom : rang à partir duquel on fait l'échange
--- accu_out_exchange.CurrentVal : -- les 4 premieres valeurs ne changent jamis
--- accu_out_exchange.Rank : rang ou on en est dans le parcours de l'échange
- localTab : arrayType;
--- localTab : tableau calculé (trié un cran plus loin)
-let
- -- je commence par trouver le minimum à partir de accu_in.CurrentRank
- accu_out_min = red<<minFromRank;size>>({MinVal = 0,
- MinRank = accu_in.CurrentRank,
- RankFrom = accu_in.CurrentRank,
- Rank = 0},
- accu_in.Tab);
-
- -- ensuite, je trouve la valeur du rang courant (rang où j'en suis
- -- de l'itération de UnarySort
- accu_out_select = red<<select;size>>({RankToFind = accu_in.CurrentRank,
- CurrentRank = 0,
- Val = 0},
- accu_in.Tab);
-
- -- puis j'échange le minimum trouvé et l'élement de rang courant
- -- (courant dans l'itération de UnarySort)
- accu_out_exchange, localTab = map_red<<Exchange_i_j;size>>({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 = {CurrentRank = accu_in.CurrentRank + 1,
- Tab = localTab};
-tel
-
-
-
-
-
-node minFromRank(accu_in : MinFR_accu; TabEltIn : elementType)
- returns (accu_out : MinFR_accu);
-let
- accu_out = {MinVal = if (accu_in.Rank<=accu_in.RankFrom)
- then TabEltIn
- else
- if (accu_in.Rank>=accu_in.RankFrom)
- -- I can start looking at TabEltIn
- then if(TabEltIn<accu_in.MinVal)
- -- I compare the current elt with
- -- the minimum of the elements already observed
- then TabEltIn
- -- the current elt is smaller,
- -- then, I remember it as the new minimum
- else accu_in.MinVal
- -- It's not a minimum,
- -- I remember the one I observed before
- else accu_in.MinVal,
- -- I'm still not in the zone of the array
- --I want to search a minimum in
- 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,
- --Never changes (rank from which I want
- -- to start the search)
- Rank = accu_in.Rank + 1
- -- Current rank for this iteration
- };
-tel
-
-
-
-
--- les acc servent juste à mémoriser les valeurs qu'on veut
-node Exchange_i_j(accu_in : Exchange_accu ; eltIn : elementType)
- returns (accu_out : Exchange_accu ; eltOut : elementType);
-let
- accu_out = {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
-
-
-
--- selection function.
-node select(accu_in : Select_accu; elt : elementType)
- returns (accu_out : Select_accu);
-let
- accu_out = {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
-
-
-
-
-
diff --git a/tests-pascal/_test-old/contractForElementSelectionInArray/readme b/tests-pascal/_test-old/contractForElementSelectionInArray/readme
deleted file mode 100644
index 6be8ce815952334469206c8b6df900a40ba7c4b9..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/contractForElementSelectionInArray/readme
+++ /dev/null
@@ -1,6 +0,0 @@
-# This file can be used as shell script command by typing "prompt> \bin\sh readme"
-
-# The command takes three lustreV6 files, the -main option with it's argument
-# and the -debug option.
-
-silus noeudsIndependants.lus main.lus packageTableau.lus -main main:main -debug
\ No newline at end of file
diff --git a/tests-pascal/_test-old/contractForElementSelectionInArray/tri.lus b/tests-pascal/_test-old/contractForElementSelectionInArray/tri.lus
deleted file mode 100644
index 479c6a7ff0106a3adf3b16d994386a76c03dfb04..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/contractForElementSelectionInArray/tri.lus
+++ /dev/null
@@ -1,225 +0,0 @@
-----------------------------------------------------
-----------------------------------------------------
---
--- Selection sort with lustre iterators
--- author : L.Morel
--- started on : 15 Mars 2002
--- last update : 3 July 2002
-----------------------------------------------------
-----------------------------------------------------
-
-
--- PARTOUT, JE SUPPOSE QUE LES ELEMENTS SONT TOUS POSITIFS
-
--- CONSTANTS
-
-const size = 10; -- size of the arrays
-
-
--- TYPES
-type INTSIZE = int^size;
-type Sort_accu = {CurrentRank : int,
- Tab : INTSIZE};
-
-type Exchange_accu = {MinVal : int,
- MinRank : int,
- RankFrom : int,
- CurrentVal : int,
- Rank : int};
-
-type Select_accu = {RankToFind : int,
- CurrentRank : int,
- Val : int};
-
-type MinFR_accu = {MinVal : int,
- MinRank : int,
- RankFrom : int,
- Rank : int};
-
-
-
--- Unary_sort takes as input an array of integers (accu_in.Tab).
--- First, it determines the minimum of the elements that are after the rank 'accu_in.currentRank'
--- in accu_in.Tab (it gets its rank and value)
--- Then it gets the current element of Tab (determinex by accu_in.currentRank) :
--- 'select' iteration
--- and switches it with the next minimum 'Exchange' iteration
--- accu_in.CurrentRank : indice permettant d'identifier les élements
--- traités jusque là. A cet étage de l'itération, on trie les élements
--- d'indice compris entre accu_in.CurrentRank et la taille du tableau -1
--- accu_in.Tab : tableau en cours de tri, Tab est tel que \forall i, j < accu_in.CurrentRank. i<j => Tab[i]<Tab[j]
--- accu_out.CurrentRank : accu_in.CurrentRank + 1 : à l'étage suivant de l'itération, on s'occupera de trier
--- les élements d'incide compris entre accu_out.CurrentRank et la taille du tableau -1
--- accu_in.Tab : tableau en cours de tri, Tab est tel que \forall i, j < accu_out.CurrentRank. i<j => Tab[i]<Tab[j]
-node UnarySort(accu_in : Sort_accu ; eltIn : int)
- returns (accu_out : Sort_accu);
-var
- accu_out_select : Select_accu;
--- accu_out_select.RankToFind : rang de l'élement dont on cherche la valeur
--- accu_out_select.CurrentRank : rang courant dans l'itération
--- accu_out_select.Val : valeur de l'élement de rang RankToFind
- accu_out_min : MinFR_accu;
--- accu_out_min.MinVal : valeur du minimum
--- accu_out_min.MinRank : rang du minimum
--- acc_out_min.RankFrom : rang à partir duquel on cherche le minimum
--- accu_out_min.Rank : rang courant (inutile en dehors de l'itération
- accu_out_exchange : Exchange_accu;
--- accu_out_exchange.MinVal : Valeur du minimum dans la tranche considérée
--- accu_out_exchange.MinRank : rang du minimum dans la tranche considérée
--- accu_out_exchange.RankFrom : rang à partir duquel on fait l'échange
--- accu_out_exchange.CurrentVal : -- les 4 premieres valeurs ne changent jamis
--- accu_out_exchange.Rank : rang ou on en est dans le parcours de l'échange
- localTab : int^size;
--- localTab : tableau calculé (trié un cran plus loin)
-let
- -- je commence par trouver le minimum à partir de accu_in.CurrentRank
- accu_out_min = red<<minFromRank;size>>(MinFR_accu{MinVal = 0,
- MinRank = accu_in.CurrentRank,
- RankFrom = accu_in.CurrentRank,
- Rank = 0},
- accu_in.Tab);
-
- -- ensuite, je trouve la valeur du rang courant (rang où j'en suis
- -- de l'itération de UnarySort
- accu_out_select = red<<select;size>>(Select_accu{RankToFind = accu_in.CurrentRank,
- CurrentRank = 0,
- Val = 0},
- accu_in.Tab);
-
- -- puis j'échange le minimum trouvé et l'élement de rang courant
- -- (courant dans l'itération de UnarySort)
- accu_out_exchange, localTab = map_red<<Exchange_i_j;size>>(
- 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
-
-
-
-
-
-node minFromRank(accu_in : MinFR_accu; TabEltIn : int)
- returns (accu_out : 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)
- -- I can start looking at TabEltIn
- then if(TabEltIn<accu_in.MinVal)
- -- I compare the current elt with
- -- the minimum of the elements already observed
- then TabEltIn
- -- the current elt is smaller,
- -- then, I remember it as the new minimum
- else accu_in.MinVal
- -- It's not a minimum,
- -- I remember the one I observed before
- else accu_in.MinVal,
- -- I'm still not in the zone of the array
- --I want to search a minimum in
- 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,
- --Never changes (rank from which I want
- -- to start the search)
- Rank = accu_in.Rank + 1
- -- Current rank for this iteration
- };
-tel
-
-
-
-
--- les acc servent juste à mémoriser les valeurs qu'on veut
-node Exchange_i_j(accu_in : Exchange_accu ; eltIn : int)
- returns (accu_out : 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
-
-
-
--- selection function.
-node select(accu_in : Select_accu; elt : int)
- returns (accu_out : 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
-
-
-
--- the main node gets an array TIn as inputs and give the corresponding sorted array Ttrie
-node main(TIn : int^size) returns (TSorted : int^size);
-var
- UnarySort_accu_out : Sort_accu;
-let
- UnarySort_accu_out = red<<UnarySort;size>>(
- Sort_accu{CurrentRank = 0,
- Tab = [7,8,4,3,2,9,1,10,2,7]}, -- Values given for test
- [7,8,4,3,2,9,1,10,2,7]); -- same
- TSorted = UnarySort_accu_out.Tab;
-tel
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
--- Property
--- is the array obtained by applying the "main" node sorted
-type sorted_iter_accu = {prev_elt : int,
- prop_is_tt : bool};
-
-
-node Sorted(TIn : int^size)
- returns (res : bool);
-var accu_out : sorted_iter_accu;
- TSorted : int^size;
-let
- TSorted = main(TIn);
- accu_out = red<<sorted_iter;size>>(sorted_iter_accu{prev_elt = 0, prop_is_tt = true}, TSorted);
- res = accu_out.prop_is_tt;
-tel
-
-
-node sorted_iter(accu_in : sorted_iter_accu; elt : int)
- returns(accu_out : 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
\ No newline at end of file
diff --git a/tests-pascal/_test-old/modelInst.lus b/tests-pascal/_test-old/modelInst.lus
deleted file mode 100644
index 9ccaffc9850c47d90ccb24718cb3f1388ba4d993..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/modelInst.lus
+++ /dev/null
@@ -1,41 +0,0 @@
--- Un modele simple
--------------------
-model m1
- needs
- type t;
-
- provides
- node n ( init, in : t ) returns ( ok : t );
-
- body
-
- node n(init, in: t) returns (ok: t);
- let
- ok = init -> pre in;
- tel
- end
-
- package Pint is m1( int );
- package Pbool is m1( bool );
- package Preal is m1( real );
-
--- le package principale definit une instance de "m1" localement
-----------------------------------------------------------------
-package main
-
- provides node main(i: int; ray : real) returns (oint: int; obool: bool; oreal: real);
-
- body
-
-
- const pi = 3.14159;
-
- node main(i: int; ray : real) returns (oint: int; obool: bool; oreal: real);
- let
- oint = Pint::n(0, i);
- obool = Pbool::n(true, i < 50);
- oreal = Preal::n(0., 0. -> pi * ray * ray);
- tel
-
- end
-
diff --git a/tests-pascal/_test-old/packages.lus b/tests-pascal/_test-old/packages.lus
deleted file mode 100644
index 0c7ec2622e1713f63eaa62d86c266a013232290e..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/packages.lus
+++ /dev/null
@@ -1,78 +0,0 @@
------------------------------
--- modSimple: un model simple
--- * necessite : un type
--- * fournit : un noeud
-----------------------------
-model modSimple
-needs
- type t;
-provides
- node fby1(init, fb: t) returns (next: t);
-body
-
-node fby1(init, fb: t) returns (next: t);
-let
- next = init -> pre fb;
-tel
-end
-
------------------------
--- qq instances de modSimple
------------------------
-package pint is modSimple(int);
-package pbool is modSimple(bool);
-package preal is modSimple(real);
-
-
---------------------------
--- un package intermediaire
--------------------------
-package inter
- uses pbool, pint, preal;
- provides
- node preced(in: selType) returns (out, out2: selType);
- const n : int;
- type selType;
-body
-
- type selType = { i: int; b: bool; r: real };
-
- -----------------------
- -- qq instances de modSimple
- -----------------------
- --package pint is modSimple(int);
- --package pbool is modSimple(bool);
- --package preal is modSimple(real);
-
- --package pSel is modSimple( { i: int; b: bool; r: real } );
-
- const n: int = -4;
- node preced(in: selType) returns (out, out2: selType);
- let
- out2 = { i = 0; b = true; r = .0}; --pSel::fby1(in);
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
- tel
-end
----------------------------
--- le package principal
---------------------------
-package mainPack
- uses inter;
- provides
- node preced(in: inter::selType) returns (out: inter::selType);
-body
-
- type T = int^N;
- const X = N;
- N : int = -2 * inter::n;
-
- -- node preced(in: bool) returns (out: bool);
- node preced(in: inter::selType) returns (out: inter::selType);
- var out2 : inter::selType;
- let
- out, out2 = inter::preced( in );
- tel
-end
-
diff --git a/tests-pascal/_test-old/packages2.lus b/tests-pascal/_test-old/packages2.lus
deleted file mode 100644
index e77f1649656adab13572ff72f7d1822c40a3e307..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/packages2.lus
+++ /dev/null
@@ -1,77 +0,0 @@
------------------------------
--- modSimple: un model simple
--- * necessite : un type
--- * fournit : un noeud
-----------------------------
-model modSimple
- needs
- type t;
- provides
- node fby1(init, fb: t) returns (next: t);
-body
-
-node fby1(init, fb: t) returns (next: t);
-let
- next = init -> pre fb;
-tel
-end
-
------------------------
--- qq instances de modSimple
------------------------
-package pint is modSimple(int);
-package pbool is modSimple(bool);
-package preal is modSimple(real);
-
-
-
---------------------------
--- un package intermediaire
--------------------------
-package inter
- uses pbool, preal;
- provides
-node preced(in: selType) returns (out, out2: selType);
-const n : int;
-type selType;
- body
-
-type selType = { i: int; b: bool; r: real };
-
- -----------------------
- -- qq instances de modSimple
- -----------------------
- --package pint is modSimple(int);
- --package pbool is modSimple(bool);
- --package preal is modSimple(real);
-
- --package pSel is modSimple( { i: int; b: bool; r: real } );
-
- const n: int = -4;
- node preced(in: selType) returns (out, out2: selType);
- let
- out2 = { i = 0; b = true; r = 0.0}; --pSel::fby1(in);
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
- tel
-end
----------------------------
--- le package principal
---------------------------
-
-node foo(in: int) returns (out : int);
-let
- out = in;
-tel
-
-const X = N;
- N : int = 8;
-
-type T = int^N;
- -- node preced(in: bool) returns (out: bool);
-node preced(in: inter::selType) returns (out: inter::selType);
-let
- out = in;
-tel
-
diff --git a/tests-pascal/_test-old/qs.lv6 b/tests-pascal/_test-old/qs.lv6
deleted file mode 100644
index 961267bff5c4e0d78ae105c061f4c4cc3201515f..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/qs.lv6
+++ /dev/null
@@ -1,68 +0,0 @@
-(*
-Version à base de map, intuitivement,
-une matrice carrée contient les dérives
-relatives : avance[i][j] = k ssi
- k occ de i depuis la dernière occ de j
-
-N.B. l'observateur est fait de telle manière que
- si not ok, la mémoire ne bouge pas
-*)
-
-node qscell<<const d: int>>(x, y: bool) returns (ok: bool);
-var c, pc : int;
-let
- pc = 0 -> pre c ;
- c = if y then 0
- else if x then pc + 1
- else pc;
- ok = (c <= d);
-tel
-
-node qsmap<<const n: int; const d: int>>(pcs: bool^n) returns (ok : bool);
-var
- qstab : bool^n^n ;
- t : bool^n^n;
-let
- t = map<<n, array_power<<n>> >>(pcs);
-
- qstab = map<<n, map<<n, qcell>> >>( t, pcs^n );
-
- ok = red<<n, red<<n, operator and>> >>(true^n, qstab);
-tel
-
-node qsmap32 = qsmap<<3,2>>;
-
-(*
-version récursive,
-*)
-
--- être qs deux à deux,
--- version (trivialement ?) correcte
-node isqs<<const d: int>>(x, y: bool) returns (ok : bool);
-var xav, yav, pxav, pyav : int;
-let
- pxav = 0 -> pre xav;
- pyav = 0 -> pre yav;
- xav = if y then 0 else if x then pxav + 1 else pxav;
- yav = if x then 0 else if y then pyav + 1 else pyav;
- ok = (xav <= d) and (yav <= d);
-tel
-
-(*
- NBP quasi-synchrone ssi isqs deux à deux...
- je sais pas faire avec des map, d'où recursion ...
- Le tout a une structure triangulaire ...
-*)
-
-node qsrec<<const n: int; const d: int>>(pcs: bool^n) returns (ok : bool);
-let
- ok = with (n=1) then true
- else qsrec<<n-1,d>>(pcs[1..n-1])
- and red<<n-1, operator and>>(true,
- map<<n-1, isqs<<d>> >>(pcs[0]^(n-1), pcs[1..n-1])
- )
- ;
-tel
-
-node qsrec32 = qsrec<<3,2>>;
-
diff --git a/tests-pascal/_test-old/readme b/tests-pascal/_test-old/readme
deleted file mode 100644
index 92c9ed56564032194544e465fbd76c57143e61fb..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/readme
+++ /dev/null
@@ -1,14 +0,0 @@
-# This file can be used as shell script command by typing
-# "prompt> \bin\sh readme"
-
-# It will launch compilation of the three example present in this
-# directory
-
-echo "-- Compiling package.lus"
-../../bin/lv6 packages.lus -main mainPack:preced
-
-echo "-- Compiling modelInst.lus"
-../../bin/lv6 modelInst.lus -main main:main
-
-echo "-- Compiling Condact.lus"
-../../bin/lv6 Condact.lus -main TestCondact:C
\ No newline at end of file
diff --git a/tests-pascal/_test-old/test.diff b/tests-pascal/_test-old/test.diff
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests-pascal/_test-old/test.exp b/tests-pascal/_test-old/test.exp
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests-pascal/_test-old/test.res b/tests-pascal/_test-old/test.res
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/tests-pascal/_test-old/tests/cons.lus b/tests-pascal/_test-old/tests/cons.lus
deleted file mode 100644
index c30dbc54ee5b275dc0406667817dc82b80a470ab..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/cons.lus
+++ /dev/null
@@ -1,15 +0,0 @@
-
-node consensus << const n : int >>
-( T : bool^n) returns ( a : bool);
-let
- a = with (n = 1)
- then T[0]
- else T[0] and consensus << n-1 >> (T[1..n-1]);
-tel
-
-node main (T : bool^4) returns (c : bool);
-let
- c = consensus<<4>>(T);
-tel
-
-node main2 = consensus<<10>>;
diff --git a/tests-pascal/_test-old/tests/const-array.lus b/tests-pascal/_test-old/tests/const-array.lus
deleted file mode 100644
index a974d9a4517a9077689ee39239220f3ac1be1135..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/const-array.lus
+++ /dev/null
@@ -1,18 +0,0 @@
-
-const true_3 = true^3 ;
-
-const false_2 = false^2;
-
-const toto = true_3 | false_2 ;
-
-const bibi = [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9 ];
-
-const revbibi = bibi[9..0];
-
-const bibi0_0 = bibi[0..0];
-
-const bibi0 = bibi[0];
-
-const pairs = bibi[0..9 step 2];
-
-const revpairs = bibi[8..0 step -2];
diff --git a/tests-pascal/_test-old/tests/const-bool.lus b/tests-pascal/_test-old/tests/const-bool.lus
deleted file mode 100644
index a1c1a05d5e2932672a2d752a1b8355b137e29f8f..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/const-bool.lus
+++ /dev/null
@@ -1,13 +0,0 @@
-(*
- calculs statiques
-*)
-
-const X = [false, true, false, true];
-const Y = [false, false, true, true];
-
-const ortab : bool^4 = X or Y;
-const andtab : bool^4 = X and Y;
-const impltab : bool^4 = X => Y;
-const xortab : bool^4 = X xor Y;
-const netab : bool^4 = X <> Y;
-const eqtab : bool^4 = X = Y;
diff --git a/tests-pascal/_test-old/tests/const-simple.lus b/tests-pascal/_test-old/tests/const-simple.lus
deleted file mode 100644
index b5b1976d2c5a063a82801cbd92767a154066943f..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/const-simple.lus
+++ /dev/null
@@ -1,35 +0,0 @@
-(*
- types, const et function simples
-*)
-
-type extern_type1, extern_type2 ;
-
-type bits3 = bool^n;
-
-type matrix = real^4^n;
-
-const n = 3;
-
-type couleur = enum { pique, carreau, trefle, coeur };
-
-type carte = struct { hauteur : int; couleur : couleur };
-
-function jouer (
- main_in : carte^5 ; sabot : carte
-) returns (
- main_out : carte^5; ecart : carte
-);
-
-const bibi : int = 42;
-
-const pi = 3.14;
-
-const eps : real = 1E-10;
-
-const ttf = [true, true, false];
-
-const ftf : bits3 = [false, true, false];
-
-const x0 = ftf[0];
- ext1, ext2 : extern_type1;
- ext3 : int;
diff --git a/tests-pascal/_test-old/tests/const-struct.lus b/tests-pascal/_test-old/tests/const-struct.lus
deleted file mode 100644
index 92515d3507ecf797f6179c6da2e1ea39f904fc42..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/const-struct.lus
+++ /dev/null
@@ -1,28 +0,0 @@
-(*
- type et constante struct
-*)
-
-type toto;
-const AA, BB : toto;
-
-type titi = struct {
- x : int = 1;
- y : toto = AA;
- z, t : bool
-};
-
-const ta = titi { x = 4; y = BB; z = true; t = false };
-
-const tb : titi = titi { z = true; x = 4; t = true; y = AA };
-
-const tc = titi { z = true; t = false };
-
-const td = titi { x = 42; z = false; t = false };
-
-(*
- extention homomorphe sur struct
-*)
-
-const td_6 = td^6;
-
-const tdx_6 = td_6.x;
diff --git a/tests-pascal/_test-old/tests/left.lus b/tests-pascal/_test-old/tests/left.lus
deleted file mode 100644
index b6786a672810462e55bd570ad4398c5bb0108e0b..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/left.lus
+++ /dev/null
@@ -1,16 +0,0 @@
-
-type truc = struct {
- a : bool^100;
- b : int
-};
-
-node toto(x : bool) returns (t : truc^3);
-let
- t[0].a[0..98 step 2][48 .. 0 step -2] = true^25;
- t[0].a[0..98 step 2][1 .. 49 step 2] = false^25;
- t[0].a[1..99 step 2][0] = true;
- t[0].a[1..99 step 2][1] = true;
- t[0].a[5..99 step 2] = false^48;
- t[0].b = 42;
- t[1..2] = (truc { a = true^100; b = 0 })^2;
-tel
diff --git a/tests-pascal/_test-old/tests/newpacks.lus b/tests-pascal/_test-old/tests/newpacks.lus
deleted file mode 100644
index 09786067563b4ed00226299c7887ad65a5907278..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/newpacks.lus
+++ /dev/null
@@ -1,77 +0,0 @@
------------------------------
--- modSimple: un model simple
--- * necessite : un type
--- * fournit : un noeud
-----------------------------
-model modSimple
-needs
- type t;
-provides
- node fby1(init, fb: t) returns (next: t);
-body
-
-node fby1(init, fb: t) returns (next: t);
-let
- next = init -> pre fb;
-tel
-end
-
------------------------
--- qq instances de modSimple
------------------------
-package pint is modSimple(int);
-package pbool is modSimple(bool);
-package preal is modSimple(real);
-
-
---------------------------
--- un package intermediaire
--------------------------
-package inter
- uses pbool, pint, preal;
- provides
- node preced(in: selType) returns (out, out2: selType);
- const n : int;
- type selType;
-body
-
- type selType = { i: int; b: bool; r: real };
-
- -----------------------
- -- qq instances de modSimple
- -----------------------
- --package pint is modSimple(int);
- --package pbool is modSimple(bool);
- --package preal is modSimple(real);
-
- --package pSel is modSimple( { i: int; b: bool; r: real } );
- const n: int = -4;
- node preced(in: selType) returns (out, out2: selType);
- let
- out2 = { i = 0; b = true; r = .0}; --pSel::fby1(in);
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
- tel
-end
----------------------------
--- le package principal
---------------------------
-package mainPack
- uses inter;
- provides
- node preced(in: inter::selType) returns (out: inter::selType);
-body
-
- type T = int^N;
- const X = N;
- N : int = -2 * inter::n;
-
- -- node preced(in: bool) returns (out: bool);
- node preced(in: inter::selType) returns (out: inter::selType);
- var out2 : inter::selType;
- let
- out, out2 = inter::preced( in );
- tel
-end
-
diff --git a/tests-pascal/_test-old/tests/node-simple.lus b/tests-pascal/_test-old/tests/node-simple.lus
deleted file mode 100644
index e11e7e61e14966606a50ed6507fa77c35360a2bd..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/node-simple.lus
+++ /dev/null
@@ -1,15 +0,0 @@
-
-const bibi : int;
-
-node toto(
- bibi : int;
- (b : int) when x
-) returns (
- c : int
-);
-var
- x : int;
-let
- x = a * b;
- c = x div 2 ;
-tel
diff --git a/tests-pascal/_test-old/tests/p.lus b/tests-pascal/_test-old/tests/p.lus
deleted file mode 100644
index 0c7ec2622e1713f63eaa62d86c266a013232290e..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/p.lus
+++ /dev/null
@@ -1,78 +0,0 @@
------------------------------
--- modSimple: un model simple
--- * necessite : un type
--- * fournit : un noeud
-----------------------------
-model modSimple
-needs
- type t;
-provides
- node fby1(init, fb: t) returns (next: t);
-body
-
-node fby1(init, fb: t) returns (next: t);
-let
- next = init -> pre fb;
-tel
-end
-
------------------------
--- qq instances de modSimple
------------------------
-package pint is modSimple(int);
-package pbool is modSimple(bool);
-package preal is modSimple(real);
-
-
---------------------------
--- un package intermediaire
--------------------------
-package inter
- uses pbool, pint, preal;
- provides
- node preced(in: selType) returns (out, out2: selType);
- const n : int;
- type selType;
-body
-
- type selType = { i: int; b: bool; r: real };
-
- -----------------------
- -- qq instances de modSimple
- -----------------------
- --package pint is modSimple(int);
- --package pbool is modSimple(bool);
- --package preal is modSimple(real);
-
- --package pSel is modSimple( { i: int; b: bool; r: real } );
-
- const n: int = -4;
- node preced(in: selType) returns (out, out2: selType);
- let
- out2 = { i = 0; b = true; r = .0}; --pSel::fby1(in);
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
- tel
-end
----------------------------
--- le package principal
---------------------------
-package mainPack
- uses inter;
- provides
- node preced(in: inter::selType) returns (out: inter::selType);
-body
-
- type T = int^N;
- const X = N;
- N : int = -2 * inter::n;
-
- -- node preced(in: bool) returns (out: bool);
- node preced(in: inter::selType) returns (out: inter::selType);
- var out2 : inter::selType;
- let
- out, out2 = inter::preced( in );
- tel
-end
-
diff --git a/tests-pascal/_test-old/tests/packages.lus b/tests-pascal/_test-old/tests/packages.lus
deleted file mode 100644
index 668a3e6c6f7af32d12842efa1f7f67b8d43988ec..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/packages.lus
+++ /dev/null
@@ -1,79 +0,0 @@
------------------------------
--- modSimple: un model simple
--- * necessite : un type
--- * fournit : un noeud
-----------------------------
-model modSimple
-needs
- type t;
-provides
- node fby1(init, fb: t) returns (next: t);
-body
-
-node fby1(init, fb: t) returns (next: t);
-let
- next = init -> pre fb;
-tel
-end
-
------------------------
--- qq instances de modSimple
------------------------
-package pint is modSimple(int);
-package pbool is modSimple(bool);
-package preal is modSimple(real);
-
-
---------------------------
--- un package intermediaire
--------------------------
-package inter
- uses pbool, pint, preal;
- provides
- node preced(in: selType) returns (out, out2: selType);
- const n : int;
- type selType;
- type toto = enum { bleu, blanc, rouge };
-body
-
- type selType = { i: int; b: bool; r: real };
-
- -----------------------
- -- qq instances de modSimple
- -----------------------
- --package pint is modSimple(int);
- --package pbool is modSimple(bool);
- --package preal is modSimple(real);
-
- --package pSel is modSimple( { i: int; b: bool; r: real } );
-
- const n: int = -4;
- node preced(in: selType) returns (out, out2: selType);
- let
- out2 = { i = 0, b = true, r = 0.0}; --pSel::fby1(in);
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
- tel
-end
----------------------------
--- le package principal
---------------------------
-package mainPack
---package preal
-uses inter;
-provides
- node preced(in: inter::selType) returns (out: inter::selType);
-body
- type T = int^N;
- const X = N;
- N : int = -2 * inter::n;
-
- -- node preced(in: bool) returns (out: bool);
- node preced(in: inter::selType) returns (out: inter::selType);
- var out2 : inter::selType;
- let
- out, out2 = inter::preced( in );
- tel
-end
-
diff --git a/tests-pascal/_test-old/tests/packs.lus b/tests-pascal/_test-old/tests/packs.lus
deleted file mode 100644
index 07e2f578dc295cc122f67a585261f546cb027aea..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/packs.lus
+++ /dev/null
@@ -1,66 +0,0 @@
-
-model modSimple
-needs
- type t;
-provides
- node fby1(init, fb: t) returns (next: t);
-body
- node fby1(init, fb: t) returns (next: t);
- let
- next = init -> pre fb;
- tel
-end
-
------------------------
--- qq instances de modSimple
------------------------
-package pint is modSimple(int);
-package pbool is modSimple(bool);
-package preal is modSimple(real);
-
-
---------------------------
--- un package intermediaire
--------------------------
-package inter
-uses pbool, pint, preal;
-provides
- node preced(in: selType) returns (out, out2: selType);
- const n : int;
- type selType;
-
- type toto = enum {X, Y} ;
-body
- type selType = { i: int; b: bool; r: real };
- const n: int = -4;
- node preced(in: selType) returns (out, out2: selType);
- let
- out2 = { i = 0, b = true, r = 0.0}; --pSel::fby1(in);
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
- tel
-end
-
----------------------------
--- le package principal
---------------------------
-
-package mainPack
-uses inter;
-body
-
- type couleurs = enum { bleu, rose, jaune };
- type T = int^N;
- const
- X = N;
- N : int = -2 * inter::n;
-
- -- node preced(in: bool) returns (out: bool);
- node preced(in: selType) returns (out: selType);
- var out2 : inter::selType;
- let
- out, out2 = inter::preced( in );
- tel
-end
-
diff --git a/tests-pascal/_test-old/tests/q.lus b/tests-pascal/_test-old/tests/q.lus
deleted file mode 100644
index f5910ec0cacad86c13558bb6de59fbb602465bf6..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/q.lus
+++ /dev/null
@@ -1,44 +0,0 @@
-
---export
-type pint::t = int;
-node pint::fby1(init, fb: pint::t) returns (next: pint::t);
-
-type pbool::t = bool;
-node pbool::fby1(init, fb: pbool::t) returns (next: pbool::t);
-
-type preal::t = real;
-node preal::fby1(init, fb: preal::t) returns (next: preal::t);
-
-const inter::n : int;
-type inter::selType;
-node inter::preced(in: inter::selType) returns (out, out2: inter::selType);
-
---defined
-node pint::fby1(init, fb: pint::t) returns (next: pint::t);
-let next = init -> pre fb; tel
-
-node pbbol::fby1(init, fb: pbbol::t) returns (next: pbbol::t);
-let next = init -> pre fb; tel
-
-node preal::fby1(init, fb: preal::t) returns (next: preal::t);
-let next = init -> pre fb; tel
-
-type inter::selType = { i: int; b: bool; r: real };
-const inter::n: int = -4;
-node inter::preced(in: inter::selType) returns (out, out2: inter::selType);
-let
- out2 = { i = 0; b = true; r = .0}; --pSel::fby1(in);
- out.i = pint::fby1(out2.i, in.i);
- out.b = pbool::fby1(out2.b, in.b);
- out.r = preal::fby1(out2.r, in.r);
-tel
-
-const mainPack::N : int = -2 * inter::n;
-const mainPack::X = mainPack::N;
-type mainPack::T = int^N;
-
-node mainPack::preced(in: inter::selType) returns (out: inter::selType);
-var out2 : inter::selType;
-let
- out, out2 = inter::preced( in );
-tel
diff --git a/tests-pascal/_test-old/tests/struct0.lus b/tests-pascal/_test-old/tests/struct0.lus
deleted file mode 100644
index 8690518f7d94870ef25aba7199da6e53b5f9cf33..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/struct0.lus
+++ /dev/null
@@ -1,9 +0,0 @@
-type Toto = struct {
- x : int = 1;
- y : int = 2
-};
-
-node bibi (dummy : int) returns (z : Toto);
-let
- z = Toto { x = 3 };
-tel
diff --git a/tests-pascal/_test-old/tests/t.lus b/tests-pascal/_test-old/tests/t.lus
deleted file mode 100644
index f48a56c34ed56b7c7a3d23fda1169e8a63867ecb..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/t.lus
+++ /dev/null
@@ -1,30 +0,0 @@
-
-const A =
- [[ 1, 2 ] , [ 3 , 4], [5, 6] ]
-+ [[ 1, 2 ] , [ 3 , 4], [5, 6] ] ;
-
-const B = if false then 1^2 else 2^2;
-
-node toto ( x : bool) returns (
- a : int^2^3;
- b : int^2
-);
-let
- a = A;
- --b = B + A[0];
- b = operator +(B,A[0]);
-tel
-
-node map2
-<<
- type t1, t2;
- const n: int;
- node n(x: t1; y: t2) returns (z: t3)
->>
-(X: t1^n; Y:t2^n) returns (Z: t3^n);
-let
- Z = with (n=1) then [ n(X[0], Y[0]) ]
- else (
- [n(X[0], Y[0])] | map2<<t1,t2,n-1>>(X[1..n-1],Y[1..n-1])
- ) ;
-tel
diff --git a/tests-pascal/_test-old/tests/t0.lus b/tests-pascal/_test-old/tests/t0.lus
deleted file mode 100644
index d0b40e09c349e4ed33dba1f1507dc8b7ede47ef9..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/t0.lus
+++ /dev/null
@@ -1,17 +0,0 @@
--- Test main node load
-
-function max(x : int; y : int) returns (mx: int);
-
-node min(x : int; y : int) returns (mn : int);
-let
- mn = if (x <= y) then x else y;
-tel
-
-node min_n<<const n: int>>
-(T : int^n) returns (mn : int);
-let
- mn = with (n = 1) then T[0]
- else min(T[0], min_n<<n-1>>(T[1..n-1]));
-tel
-
-node min_4 = min_n<<4>>;
diff --git a/tests-pascal/_test-old/tests/t1.lus b/tests-pascal/_test-old/tests/t1.lus
deleted file mode 100644
index 1e84660ea25aeef0da4352895239f174a6222cc5..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/t1.lus
+++ /dev/null
@@ -1,41 +0,0 @@
-
-node consensus << const n : int >>
-( T : bool^n) returns ( a : bool);
-let
- a = with (n = 1)
- then T[0]
- else T[0] and consensus << n-1 >> (T[1..n-1]);
-tel
-
-(*
-Et pourquoi pas étendre la notion de params statiques ???
-*)
-
-node fold_left <<
- type t1;
- type t2;
- const n : int;
- node treat (x:t1; y:t2) returns (z:t1)
->>
-(
- a : t1; X : t2^n
-) returns (
- c : t1
-);
-let
- c = with (n = 0) then a
- else
- fold_left << t1, t2, n-1, treat >> (
- treat(a, X[0]),
- X[1..n-1]
- );
-tel
-
-node bt_void<<const n>>(t : bool^n) returns (x : bool);
-let
- x = fold<<operator or>>(false, t);
-tel
-
-node bt_void<<const n>>(t : bool^n) = fold<<operator or>>(false, t);
-
-node bt_void(t : bool array) = fold<<operator or>>(false, t);
diff --git a/tests-pascal/_test-old/tests/t2.lus b/tests-pascal/_test-old/tests/t2.lus
deleted file mode 100644
index 246ea20fa35ba7b37dc8ef95c8603510e9bc0410..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/t2.lus
+++ /dev/null
@@ -1,54 +0,0 @@
-
-node consensus <<
- const n : int
->>
-(
- T : bool^n
-) returns (
- a : bool
-);
-let
- a = with (n = 1)
- then T[0]
- else T[0] and consensus <<n-1>> (T[1..n-1]);
-tel
-
-(*
-Et pourquoi pas étendre la notion de params statiques ???
-*)
-
-node fold_left <<
- type t1;
- type t2;
- const n : int;
- node treat(x:t1; y:t2) returns (z:t1)
->> (
- a : t1; X : t2^n
-) returns (
- c : t1
-);
-let
- c = with (n = 0) then a
- else
- fold_left << t1, t2, n-1, treat >> (
- treat(a, X[0]),
- X[1..n-1]
- );
-tel
-
--- Alors :
-node consensus_6(X : bool^6) returns (c : bool);
-let
- c = fold_left << bool,bool,6, operator and >>(true, X);
-tel
-
--- Voire même :
-
-node consensus_6_bis = fold_left << bool,bool,6, operator and >> ;
-
--- Ou encore :
-
-node consensus_bis << const n : int >> =
- fold_left << bool,bool,n, operator and >> ;
-
-
diff --git a/tests-pascal/_test-old/tests/test.lus b/tests-pascal/_test-old/tests/test.lus
deleted file mode 100644
index 54b7877805880910c796b29037c587e499276828..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/test.lus
+++ /dev/null
@@ -1,9 +0,0 @@
-
-package P1
-provides
- const y : int;
- type titi;
-body
- const y : int = 3;
- type titi = int^(y + 2);
-end
diff --git a/tests-pascal/_test-old/tests/trivial.lus b/tests-pascal/_test-old/tests/trivial.lus
deleted file mode 100644
index aa4df09edf5296d0c4224fc1cbdcef0886d9f240..0000000000000000000000000000000000000000
--- a/tests-pascal/_test-old/tests/trivial.lus
+++ /dev/null
@@ -1,4 +0,0 @@
-node trivial(x : int) returns (y : int);
-let
- y = 1;
-tel
diff --git a/tests-pascal/moretests/Makefile b/tests-pascal/moretests/Makefile
deleted file mode 100644
index 3bb12357d44b66bbc6000dd4a353c905456d2088..0000000000000000000000000000000000000000
--- a/tests-pascal/moretests/Makefile
+++ /dev/null
@@ -1,135 +0,0 @@
-
-OBJDIR=../obj$(HOSTTYPE)
-
-LC0=$(OBJDIR)/lus2lic
-LC=$(OBJDIR)/lus2lic -vl 2
-LC2=$(OBJDIR)/lus2lic
-
-NL="----------------------------------------------------------------------\\n"
-filter_line=grep -v Opening\ file
-
-OK_LUS=$(shell find should_work -name "*.lus" -print | LC_ALL=C sort -n)
-
-KO_LUS=$(shell find should_fail -name "*.lus" -print | LC_ALL=C sort -n)
-
-ALL_LUS=$(OK_LUS) $(KO_LUS)
-
-LIC=$(shell find should_work -name "*.lic" -print | LC_ALL=C sort -n)
-
-
-when:
- for d in ${ALL_LUS}; do \
- ls $$d; \
- grep -n " when" $$d; \
- done
-tgz:
- tar cvfz lustre_non_reg_files.tgz should_work should_fail
-
-
-lic:
- /bin/echo "generate all possible lic files"
- for d in ${OK_LUS}; do \
- /bin/echo -e "\n$(NL)====> $(LC2) $$d -o $$d.lic " ;\
- $(LC2) $$d -o $$d.lic ;\
- done
-
-xxx:
- /bin/echo "reentrant ?"
- for d in ${LIC}; do \
- /bin/echo -e "\n$(NL)====> $(LC2) $$d " ;\
- $(LC2) $$d > /dev/null ;\
- done
-
-
-begin:
- /bin/echo "Non-regression tests" > test_ok.res
- /bin/echo "Those tests are supposed to generate errors" > test_ko.res
-
-
-unit:
- $(LC0) -unit >> test_ok.res 2>&1
-
-help:
- $(LC0) -help >> test_ok.res 2>&1
-
-version:
- $(LC0) --version
-
-FILTER= grep -v "file was generated by" | grep -v " on " | grep -v "Opening file "
-
-do_not_exist:
- $(LC) do_not_exist.lus | $(FILTER) >> test_ko.res 2>&1 || true
-
-test_lic: begin unit help version do_not_exist
- for d in ${OK_LUS}; do \
- /bin/echo -e "\n$(NL)====> $(LC) --nonreg-test $$d" >> test_ok.res; \
- $(LC) --nonreg-test $$d >> test_ok.res 2>&1 ;\
- done; \
- for d in ${KO_LUS}; do \
- /bin/echo -e "\n$(NL)====> $(LC) --nonreg-test $$d" >> test_ko.res; \
- $(LC) --nonreg-test $$d >> test_ko.res 2>&1 ;\
- done; \
- rm -f test.res ; cat test_ok.res test_ko.res | $(FILTER) > test.res ;\
- diff -u test.res.exp test.res > test.diff || \
- (cat test.diff ; /bin/echo "cf test.diff"; exit 1)
-utest_lic:
- cp test.res test.res.exp
-
-
-errors_nb:
- /bin/echo -e "There were $(shell grep Error test_ok.res | wc -l) errors."
- /bin/echo -e "There were $(shell grep Warning test_ok.res | wc -l) Warnings."
-
-errors:errors_nb
- /bin/echo -e "There were $(shell grep Warning test_ok.res | wc -l) Warnings."
- grep Warning test_ok.res || true
- /bin/echo -e "There were $(shell grep Error test_ok.res | wc -l) errors."
- grep "*** Error" test_ok.res
-
-
-
-
-
-test_ec:
- rm -f test_ec.res
- for d in ${OK_LUS}; do \
- /bin/echo -e "\n$(NL)====> $(LC0) --nonreg-test -ec $$d -o /tmp/xx.ec" >> test_ec.res; \
- $(LC0) -ec --nonreg-test $$d -o /tmp/xx.ec >> test_ec.res 2>&1 ;\
- /bin/echo -e "ec2c /tmp/xx.ec" >> test_ec.res; \
- (ec2c /tmp/xx.ec >> test_ec.res 2>&1 && /bin/echo -n "ok ") || /bin/echo " KO ($$d)!";\
- done; \
- diff -u test_ec.res.exp test_ec.res > test_ec.diff || \
- (cat test_ec.diff ; /bin/echo "cf test_ec.diff"; exit 1)
-
-
-utest_ec:
- cp test_ec.res test_ec.res.exp
-
-test_lv4:
- rm test_lv4.res || /bin/echo "";
- for d in ${OK_LUS}; do \
- /bin/echo -e "\n$(NL)====> $(LC0) --nonreg-test -lv4 $$d -o /tmp/xx.lus" >> test_lv4.res; \
- $(LC0) --nonreg-test -lv4 $$d -o /tmp/xx.lus >> test_lv4.res 2>&1 ;\
- if [ ! -f /tmp/xx.lus ]; then echo "Error $$d: no /tmp/xx.lus file" >> test_lv4.res 2>&1; fi ;\
- for node in `lusinfo /tmp/xx.lus nodes`; do \
- /bin/echo -e "lus2ec /tmp/xx.lus $$node" >> test_lv4.res; \
- (lus2ec /tmp/xx.lus $$node >> \
- test_lv4.res 2>&1 && /bin/echo -n "ok ") \
- || /bin/echo " KO ($$d)!";\
- done; \
- done; \
- diff -u test_lv4.res.exp test_lv4.res > test_lv4.diff || \
- (cat test_lv4.diff ; /bin/echo "cf test_lv4.diff"; exit 1)
-
-
-utest_lv4:
- cp test_lv4.res test_lv4.res.exp
-
-test: test_lic test_ec test_lv4
-utest: utest_lic utest_ec utest_lv4
-
-
-clean:
- for d in ${ALL_LUS}; do \
- rm $$d.lic; \
- done
diff --git a/tests-pascal/moretests/should_fail/misc/wrongmap.lus b/tests-pascal/moretests/should_fail/misc/wrongmap.lus
deleted file mode 100644
index c4dc3c2941d1bba5e34627ad9cb4c03f4347b945..0000000000000000000000000000000000000000
--- a/tests-pascal/moretests/should_fail/misc/wrongmap.lus
+++ /dev/null
@@ -1,6 +0,0 @@
-
-
-node overplus = map<<+,4>>;
-
-node do_bool(x,y: bool^4) returns (o: bool^4);
-let o = overplus(x,y); tel
diff --git a/tests-pascal/moretests/should_work/aliases/alias.lus b/tests-pascal/moretests/should_work/aliases/alias.lus
deleted file mode 100644
index 1fe4d82fba3d1c9b7350961a1f48e385f466ba1d..0000000000000000000000000000000000000000
--- a/tests-pascal/moretests/should_work/aliases/alias.lus
+++ /dev/null
@@ -1,22 +0,0 @@
-
-
-const toto = 42;
-
-const huit = 9; -- gnark gnark
-
-type t = enum { Bleu, Blanc };
-
-type a = int^toto;
-
-const c : t = Bleu;
-const c2 : t;
-
-type t1 = bool^4^5;
-
-type bool_4 ; -- Ah ah !!
-type bool_4a ; -- Ah ah !!
-type bool_4b ; -- Ah ah !!
-
-type str = { foo: t^toto^huit; bar : t1 };
-
-
diff --git a/tests-pascal/moretests/should_work/aliases/ex.lus b/tests-pascal/moretests/should_work/aliases/ex.lus
deleted file mode 100644
index 6cd5764fc7c5f1810f97c561a64e7427d3ed182a..0000000000000000000000000000000000000000
--- a/tests-pascal/moretests/should_work/aliases/ex.lus
+++ /dev/null
@@ -1,10 +0,0 @@
-type
- t = int^1^2^3^4;
- t1 = t^4;
- t2 = {a: int; b: bool^11^22};
- s1 = {x:int; y:t};
- s = {x:t; y:s1};
-node ex(a: s) returns (b: int);
-let
- b = a.x[0][0][0][0] + a.y.y[0][0][0][0];
-tel
diff --git a/tests-pascal/moretests/test.res.exp b/tests-pascal/moretests/test.res.exp
deleted file mode 100644
index 8136841aec96ba48e2f78fe536ba740999956687..0000000000000000000000000000000000000000
--- a/tests-pascal/moretests/test.res.exp
+++ /dev/null
@@ -1,113 +0,0 @@
-Non-regression tests
-usage: lus2lic [options] <file> | lus2lic -help
-
--n, -node <string>
- Set the main node (all items are compiled if unset)
--o, --output-file <string>
- Set the output file name
--knc, --keep-nested-calls
- Keep nested calls. By default, only one node per equation is generated.
--ei, --expand-iterators
- Expand array iterators (i.e., generate iterator-free code).
--ee, --expand-enums
- Translate enums into integers.
--esa, --expand-structs-and-arrays
- Expand structures and arrays using as many variables as necessary (automatically impose '-ei')
--en, --expand-nodes
- Expand the main node (use the first node if no one is specified).
--den, --do_not-expand-nodes <string>
- Do not expand node (useful in the expand mode only of course).
--lv4, --lustre-v4
- Use Lustre V4 syntax (automatically impose '-ei -ee -esa').
--ec, --expanded-code
- Generate ec (actually just an alias for '-en -lv4 --no-prefix').
--np, --no-prefix
- Do not prefix variable names by their module (beware: variable names may clash with this option).
--version, --version
- Print the current version and exit
--v, --verbose
- Set the verbose level to 1
--vl <int> Set the verbose level
--more Show hidden options (for dev purposes)
-
-----------------------------------------------------------------------
-====> ../objlinux/lus2lic -vl 2 --nonreg-test should_work/aliases/alias.lus
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
--- ../objlinux/lus2lic -vl 2 --nonreg-test should_work/aliases/alias.lus
-type bool_4 = bool^4 (*abstract in the source*);
-type bool_4_5 = bool_4^5 (*abstract in the source*);
-type alias::a = int^42;
-type alias::bool_4;
-type alias::bool_4a;
-type alias::bool_4b;
-type alias::str = struct {foo : alias::t_42_9; bar : bool_4_5};
-type alias::t = enum {alias::Bleu, alias::Blanc};
-type alias::t1 = bool_4^5;
-type alias::t_42 = alias::t^42 (*abstract in the source*);
-type alias::t_42_9 = alias::t_42^9 (*abstract in the source*);
-const alias::c2 : alias::t;
-const alias::huit = 9;
-const alias::toto = 42;
-
-----------------------------------------------------------------------
-====> ../objlinux/lus2lic -vl 2 --nonreg-test should_work/aliases/ex.lus
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: LazyCompiler.lookup_node_exp_eff: node key 'ex::ex' NOT FOUND
-#DBG: LazyCompiler.lookup_node_exp_eff: node key 'ex::ex' NOT FOUND
-#DBG: LazyCompiler.node_check_do 'ex::ex' (in file "ex.lus", line 0, col 0 to 0, token 'compile all items')
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f (anynum * anynum) with (int * int) gives Unif with any(num) = int
-#DBG: UnifyType.f (anynum * anynum) with (int * int) gives Unif with any(num) = int
--- ../objlinux/lus2lic -vl 2 --nonreg-test should_work/aliases/ex.lus
-type bool_11 = bool^11 (*abstract in the source*);
-type bool_11_22 = bool_11^22 (*abstract in the source*);
-type int_1 = int^1 (*abstract in the source*);
-type int_1_2 = int_1^2 (*abstract in the source*);
-type int_1_2_3 = int_1_2^3 (*abstract in the source*);
-type int_1_2_3_4 = int_1_2_3^4 (*abstract in the source*);
-type ex::s = struct {x : int_1_2_3_4; y : ex::s1};
-type ex::s1 = struct {x : int; y : int_1_2_3_4};
-type ex::t = int_1_2_3^4;
-type ex::t1 = int_1_2_3_4^4;
-type ex::t2 = struct {a : int; b : bool_11_22};
-node ex::ex(a:ex::s) returns (b:int);
-let
- b = a.x[0][0][0][0] + a.y.y[0][0][0][0];
-tel
--- end of node ex::ex
-Those tests are supposed to generate errors
-
-----------------------------------------------------------------------
-====> ../objlinux/lus2lic -vl 2 --nonreg-test should_fail/misc/wrongmap.lus
-#DBG: LazyCompiler.lookup_node_exp_eff: node key 'wrongmap::do_bool' NOT FOUND
-#DBG: LazyCompiler.lookup_node_exp_eff: node key 'wrongmap::do_bool' NOT FOUND
-#DBG: LazyCompiler.node_check_do 'wrongmap::do_bool' (in file "wrongmap.lus", line 0, col 0 to 0, token 'compile all items')
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: UnifyType.f () with () gives Equal
-#DBG: LazyCompiler.lookup_node_exp_eff: node key 'wrongmap::overplus' NOT FOUND
-#DBG: LazyCompiler.node_check_do 'wrongmap::overplus' (in file "wrongmap.lus", line 6, col 9 to 16, token 'overplus')
-#DBG: UnifyType.f () with () gives Equal
-#DBG: GetEff.translate_val_exp CALL_n 'overplus gives type: anynum^4 * anynum^4 -> anynum^4
-#DBG: UnifyType.f (anynum^4 * anynum^4) with (bool^4 * bool^4) gives Ko
-*** Error in file "wrongmap.lus", line 6, col 9 to 16, token 'overplus':
-*** type error:
-*** while unifing (anynum^4 * anynum^4) with (bool^4 * bool^4)
-*** get 'bool' where 'int' or 'real' was expected
-