From 09992e2232efd2435b22f0e10f76eb5b01d1e72b Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Fri, 10 May 2013 17:01:55 +0200
Subject: [PATCH] Handle polymorphic soc better
I though polymorphism was removed by l2lRmPoly.ml, but well, it was easy.
nb : #FAILS=131->128
---
src/main.ml | 7 ++++---
src/soc.ml | 25 ++++++++++++++++++++++---
src/socExecEvalPredef.ml | 22 ++++++++++++++++------
src/socPredef.ml | 4 +++-
test/lus2lic.sum | 12 ++++++------
test/should_work/consensus2.lus | 2 +-
test/should_work/mappredef.lus | 5 +++--
test/should_work/param_node.lus | 2 +-
test/should_work/testPilote.lus | 2 +-
todo.org | 6 ++++++
10 files changed, 63 insertions(+), 24 deletions(-)
diff --git a/src/main.ml b/src/main.ml
index d17ab2bf..dd321012 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 06/05/2013 (at 11:14) by Erwan Jahier> *)
+(* Time-stamp: <modified the 10/05/2013 (at 15:00) by Erwan Jahier> *)
open Verbose
open AstV6
@@ -131,7 +131,7 @@ let (gen_autotest_files : LicPrg.t -> Ident.idref option -> Lv6MainArgs.t -> uni
flush stdout
-let main = (
+let main () = (
(* Compile.init_appli () ; *)
(* parse_args (); *)
let opt = Lv6MainArgs.parse Sys.argv in
@@ -229,4 +229,5 @@ let main = (
close_out opt.oc
-);
+);;
+main();
diff --git a/src/soc.ml b/src/soc.ml
index f7d63431..165648af 100644
--- a/src/soc.ml
+++ b/src/soc.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 08/04/2013 (at 14:10) by Erwan Jahier> *)
+(* Time-stamp: <modified the 10/05/2013 (at 16:21) by Erwan Jahier> *)
(** Synchronous Object Component *)
@@ -83,15 +83,33 @@ type t = {
(* Do this soc have a memory (pre, fby) + its type + default value *)
}
+
+
+let (compare_soc_key : key -> key -> int) =
+ fun (id1, tl1, si1) (id2, tl2, si2) ->
+ let rec unifiable tl1 tl2 =
+ (* Very simple version that is correct only for keys that
+ contain at most 1 polymorphic var, which is currently the
+ case for v6 programs *)
+ match tl1,tl2 with
+ | [],[] -> true
+ | _::tl1, Data.Alpha(_)::tl2
+ | Data.Alpha(_)::tl1, _::tl2 -> unifiable tl1 tl2
+ | t1::tl1, t2::tl2 -> t1=t2 && unifiable tl1 tl2
+ | _,_ -> false
+ in
+ if unifiable tl1 tl2
+ then compare (id1, si1) (id2, si2)
+ else compare (id1, tl1, si1) (id2, tl2, si2)
+
(* SocKeyMap ? *)
module SocMap = Map.Make(
struct
type t = key
- let compare = compare
+ let compare = compare_soc_key
end
)
-
type tbl = t SocMap.t
let cpt = ref 0
@@ -101,3 +119,4 @@ let (make: key -> instance) =
let instance = Printf.sprintf "%s%03d" id !cpt in
incr cpt;
instance,sk
+
diff --git a/src/socExecEvalPredef.ml b/src/socExecEvalPredef.ml
index 04af1004..6de5a119 100644
--- a/src/socExecEvalPredef.ml
+++ b/src/socExecEvalPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 07/05/2013 (at 15:45) by Erwan Jahier> *)
+(* Time-stamp: <modified the 10/05/2013 (at 16:21) by Erwan Jahier> *)
open SocExecValue
open Data
@@ -297,21 +297,31 @@ let lustre_hat tl ctx =
let (get: Soc.key -> (ctx -> ctx)) =
fun (n,tl,si_opt) ->
match n with
+ | "Lustre::rplus"
+ | "Lustre::iplus"
| "Lustre::plus" -> lustre_plus
+ | "Lustre::itimes"
+ | "Lustre::rtimes"
| "Lustre::times"-> lustre_times
+ | "Lustre::idiv"
+ | "Lustre::rdiv"
| "Lustre::div" -> lustre_div
+ | "Lustre::iminus"
+ | "Lustre::rminus"
| "Lustre::minus"-> lustre_minus
| "Lustre::mod" -> lustre_mod
+ | "Lustre::iuminus"
+ | "Lustre::ruminus"
| "Lustre::uminus" -> lustre_uminus
| "Lustre::not" -> lustre_not
| "Lustre::real2int" -> lustre_real2int
| "Lustre::int2real" -> lustre_int2real
- | "Lustre::lt" -> lustre_lt
- | "Lustre::gt" -> lustre_gt
- | "Lustre::lte" -> lustre_lte
- | "Lustre::gte" -> lustre_gte
+ | "Lustre::lt"| "Lustre::rlt" | "Lustre::ilt" -> lustre_lt
+ | "Lustre::gt"| "Lustre::rgt" | "Lustre::igt" -> lustre_gt
+ | "Lustre::lte"| "Lustre::rlte" | "Lustre::ilte" -> lustre_lte
+ | "Lustre::gte"| "Lustre::rgte"| "Lustre::igte" -> lustre_gte
| "Lustre::xor" -> lustre_xor
| "Lustre::and" -> lustre_and
@@ -321,7 +331,7 @@ let (get: Soc.key -> (ctx -> ctx)) =
| "Lustre::impl" -> lustre_impl
- | "Lustre::if" -> lustre_if
+ | "Lustre::if"| "Lustre::rif"| "Lustre::iif" -> lustre_if
| "Lustre::hat" -> lustre_hat tl
| "Lustre::array" -> lustre_array tl
diff --git a/src/socPredef.ml b/src/socPredef.ml
index 9ed2d2f1..a1f7d2d5 100644
--- a/src/socPredef.ml
+++ b/src/socPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 07/05/2013 (at 15:20) by Erwan Jahier> *)
+(* Time-stamp: <modified the 10/05/2013 (at 14:52) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
@@ -115,11 +115,13 @@ let of_soc_key : Soc.key -> Soc.t =
let sp_nary = soc_profile_of_types_nary in
match id with
| "Lustre::mod" -> (make_soc sk (sp tl) [step11])
+ | "Lustre::iuminus"
| "Lustre::uminus" -> (make_soc sk (sp tl) [step11])
| "Lustre::not" -> (make_soc sk (sp tl) [step11])
| "Lustre::real2int" -> (make_soc sk (sp tl) [step11])
| "Lustre::int2real" -> (make_soc sk (sp tl) [step11])
+ | "Lustre::iplus"
| "Lustre::plus" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::times" -> (make_soc sk (sp tl) [step21 None])
| "Lustre::div" -> (make_soc sk (sp tl) [step21 None])
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index e2952e09..588ab886 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Tue May 7 17:03:33 2013
+Test Run By jahier on Fri May 10 16:53:20 2013
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
@@ -100,7 +100,7 @@ UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/aux.lus
PASS: ./lus2lic {-o /tmp/consensus2.lic should_work/consensus2.lus}
PASS: ./lus2lic {-ec -o /tmp/consensus2.ec should_work/consensus2.lus}
PASS: ./ec2c {-o /tmp/consensus2.c /tmp/consensus2.ec}
-FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/consensus2.lus
+PASS: ../utils/test_lus2lic_no_node should_work/consensus2.lus
PASS: ./lus2lic {-o /tmp/dependeur.lic should_work/dependeur.lus}
PASS: ./lus2lic {-ec -o /tmp/dependeur.ec should_work/dependeur.lus}
PASS: ./ec2c {-o /tmp/dependeur.c /tmp/dependeur.ec}
@@ -108,7 +108,7 @@ UNRESOLVED: Time out: ../utils/test_lus2lic_no_node should_work/dependeur.lus
PASS: ./lus2lic {-o /tmp/mappredef.lic should_work/mappredef.lus}
PASS: ./lus2lic {-ec -o /tmp/mappredef.ec should_work/mappredef.lus}
PASS: ./ec2c {-o /tmp/mappredef.c /tmp/mappredef.ec}
-FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/mappredef.lus
+PASS: ../utils/test_lus2lic_no_node should_work/mappredef.lus
PASS: ./lus2lic {-o /tmp/call06.lic should_work/call06.lus}
PASS: ./lus2lic {-ec -o /tmp/call06.ec should_work/call06.lus}
PASS: ./ec2c {-o /tmp/call06.c /tmp/call06.ec}
@@ -968,7 +968,7 @@ PASS: ../utils/test_lus2lic_no_node should_work/trivial2.lus
PASS: ./lus2lic {-o /tmp/param_node.lic should_work/param_node.lus}
PASS: ./lus2lic {-ec -o /tmp/param_node.ec should_work/param_node.lus}
PASS: ./ec2c {-o /tmp/param_node.c /tmp/param_node.ec}
-FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/param_node.lus
+PASS: ../utils/test_lus2lic_no_node should_work/param_node.lus
PASS: ./lus2lic {-o /tmp/simple.lic should_work/simple.lus}
PASS: ./lus2lic {-ec -o /tmp/simple.ec should_work/simple.lus}
PASS: ./ec2c {-o /tmp/simple.c /tmp/simple.ec}
@@ -1045,8 +1045,8 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
=== lus2lic Summary ===
-# of expected passes 832
-# of unexpected failures 131
+# of expected passes 835
+# of unexpected failures 128
# of unexpected successes 11
# of expected failures 37
# of unresolved testcases 22
diff --git a/test/should_work/consensus2.lus b/test/should_work/consensus2.lus
index 5d15c9fa..579aeba6 100644
--- a/test/should_work/consensus2.lus
+++ b/test/should_work/consensus2.lus
@@ -5,4 +5,4 @@ let
else T[0] and consensus << n-1 >> (T[1 .. n-1]);
tel
-node main = consensus<<8>>;
\ No newline at end of file
+node consensus2 = consensus<<8>>;
\ No newline at end of file
diff --git a/test/should_work/mappredef.lus b/test/should_work/mappredef.lus
index 03b0b071..89f19d45 100644
--- a/test/should_work/mappredef.lus
+++ b/test/should_work/mappredef.lus
@@ -1,5 +1,6 @@
const N = 3;
-type tab_int = int^N;
+type tab_real = int^N;
+ tab_int = int^N;
tab_bool = bool^N;
node mappredef(x: tab_bool; a, b: tab_int) returns (c, d: tab_int);
@@ -8,5 +9,5 @@ node mappredef(x: tab_bool; a, b: tab_int) returns (c, d: tab_int);
let
z = if(x[0]) then a[0] else b[0] ;
c = map<<Lustre::if, N>>(x, a, b);
- d = map<<Lustre::iuminus, N>>(b);
+ d = map<<Lustre::uminus, N>>(b);
tel
diff --git a/test/should_work/param_node.lus b/test/should_work/param_node.lus
index 433b4507..3bb62f4f 100644
--- a/test/should_work/param_node.lus
+++ b/test/should_work/param_node.lus
@@ -8,4 +8,4 @@ let
v = f(a, 1);
x = v ^ n;
tel ---
-node toto_3 = toto_n<<Lustre::iplus, 3>>;
+node param_node = toto_n<<Lustre::iplus, 3>>;
diff --git a/test/should_work/testPilote.lus b/test/should_work/testPilote.lus
index 2e8e60ea..e93dbd12 100644
--- a/test/should_work/testPilote.lus
+++ b/test/should_work/testPilote.lus
@@ -1,4 +1,4 @@
-package pilote
+package testPilote
provides
node testPilote(Hpilote, semAutP : bool; --
diff --git a/todo.org b/todo.org
index 0e7bff65..793e539d 100644
--- a/todo.org
+++ b/todo.org
@@ -130,6 +130,12 @@ l'appel depuis l'oracle au noeud à tester est mal typé...
** TODO lus2lic -ee -exec devrait utiliser des enums (a la ecexe)
- State "TODO" from "" [2013-05-07 Tue 16:36]
+** TODO le test des programmes packagé ne fonctionne pas
+ - State "TODO" from "" [2013-05-10 Fri 10:52]
+modifer
+file:~/lus2lic/utils/test_lus2lic_no_node
+
+
* Divers
** TODO lic2c : le jour ou on genere du code C, y'a peut-etre des trucs a recuperer
- State "TODO" from "" [2012-12-10 Mon 14:32]
--
GitLab