From 53e5bb83bd37e5ded08a44280c102043aea647d3 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Fri, 31 May 2013 15:58:50 +0200
Subject: [PATCH] Fix an internal error that was actually occuring on faulty
programs when the arity of an alias node was wrong.
---
src/socExec.ml | 6 ++-
src/unifyType.ml | 88 ++++++++++++++++++------------------
test/lus2lic.sum | 17 ++++---
test/lus2lic.time | 4 +-
test/should_fail/type/t1.lus | 44 ++++++++++++++++++
test/should_work/t1.lus | 10 ++--
todo.org | 27 ++---------
todo.org_archive | 55 ++++++++++++++++++++++
8 files changed, 169 insertions(+), 82 deletions(-)
create mode 100644 test/should_fail/type/t1.lus
diff --git a/src/socExec.ml b/src/socExec.ml
index e615acf5..682f5a65 100644
--- a/src/socExec.ml
+++ b/src/socExec.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 24/05/2013 (at 09:55) by Erwan Jahier> *)
+(* Time-stamp: <modified the 31/05/2013 (at 13:59) by Erwan Jahier> *)
open Soc
open Data
@@ -199,7 +199,9 @@ and expand_var enum_flag var = match var with
done;
(expand_profile enum_flag !res)
| (vn,Struct(name,fl)) -> expand_profile enum_flag (List.map (fun (fn,t) -> vn^"_"^fn,t ) fl)
- | (vn,Extern id) -> assert false (* finish me! *)
+ | (vn,Extern id) ->
+ print_string "Extern node not yet supported, sorry\n"; flush stdout;
+ assert false (* finish me! *)
| (vn,Alpha _) -> assert false (* should not occur *)
let (int_to_enum : Data.v -> Soc.ident list -> Data.v) =
diff --git a/src/unifyType.ml b/src/unifyType.ml
index 53bca868..99499a11 100644
--- a/src/unifyType.ml
+++ b/src/unifyType.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 17/05/2013 (at 10:56) by Erwan Jahier> *)
+(* Time-stamp: <modified the 31/05/2013 (at 15:43) by Erwan Jahier> *)
(*
12/07. Premier pas vers une méthode un peu plus standard :
@@ -59,62 +59,64 @@ Inutile d'essayer de ressembler à un vrai algo d'unification de type :
et un given, et on doit arriver à s'en sortir ...
*)
let f (l1: Lic.type_ list) (l2: Lic.type_ list): t =
- let rec unify_type_eff (t1:Lic.type_) (t2: Lic.type_) : t =
- if t1 = t2 then Equal else
+ let rec unify_type_eff (t1:Lic.type_) (t2: Lic.type_) : t =
+ if t1 = t2 then Equal else
match (t1,t2) with
- | Array_type_eff(teff_ext1,i1), Array_type_eff(teff_ext2,i2) ->
- if i1 <> i2 then Ko "\n*** incompatible array size"
- else unify_type_eff teff_ext1 teff_ext2
- | Struct_type_eff(l1, fl1), Struct_type_eff(l2, fl2) ->
- if l1 <> l2 then Ko "\n*** incompatible structure" else
+ | Array_type_eff(teff_ext1,i1), Array_type_eff(teff_ext2,i2) ->
+ if i1 <> i2 then Ko "\n*** incompatible array size"
+ else unify_type_eff teff_ext1 teff_ext2
+ | Struct_type_eff(l1, fl1), Struct_type_eff(l2, fl2) ->
+ if l1 <> l2 then Ko "\n*** incompatible structure" else
(** USELESS ??? *)
let fl1 = List.map (fun (_,(te,_)) -> te) fl1
and fl2 = List.map (fun (_,(te,_)) -> te) fl2 in
assert(List.length fl1 = List.length fl1);
List.fold_left2 unify_do_acc Equal fl1 fl2
- | TypeVar AnyNum, TypeVar Any
- | TypeVar Any, TypeVar AnyNum -> Unif (TypeVar AnyNum)
- | t, TypeVar Any | (TypeVar Any), t ->
- if contains t (TypeVar Any) || contains t (TypeVar AnyNum) then
+ | TypeVar AnyNum, TypeVar Any
+ | TypeVar Any, TypeVar AnyNum -> Unif (TypeVar AnyNum)
+ | t, TypeVar Any | (TypeVar Any), t ->
+ if contains t (TypeVar Any) || contains t (TypeVar AnyNum) then
Ko(("\n*** " ^ teff2str t1) ^ " and " ^ (teff2str t2) ^
- " are not unifiable (there is a cycle)")
- else Unif t
- | t, TypeVar AnyNum
- | TypeVar AnyNum, t ->
- if contains t (TypeVar Any) || contains t (TypeVar AnyNum) then
+ " are not unifiable (there is a cycle)")
+ else Unif t
+ | t, TypeVar AnyNum
+ | TypeVar AnyNum, t ->
+ if contains t (TypeVar Any) || contains t (TypeVar AnyNum) then
Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^
- " are not unifiable (there is a cycle)")
- else if is_overloadable t then Unif t
- else
+ " are not unifiable (there is a cycle)")
+ else if is_overloadable t then Unif t
+ else
Ko("\n*** get '" ^ (teff2str t) ^ "' where 'int' or 'real' was expected")
- | _ ->
- Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^
- " are not unifiable")
+ | _ ->
+ Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^
+ " are not unifiable")
and (unify_do_acc: t -> Lic.type_ -> Lic.type_ -> t) =
fun acc te1 te2 ->
match acc, unify_type_eff te1 te2 with
- | Equal, Equal -> Equal
- | Ko msg, _
- | _, Ko msg -> Ko msg
- | Unif t, Equal
- | Equal, Unif t -> Unif t
- | Unif t1, Unif t2 -> if t1 = t2 then acc else
- Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^
- " are not unifiable")
+ | Equal, Equal -> Equal
+ | Ko msg, _
+ | _, Ko msg -> Ko msg
+ | Unif t, Equal
+ | Equal, Unif t -> Unif t
+ | Unif t1, Unif t2 -> if t1 = t2 then acc else
+ Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^
+ " are not unifiable")
in
- Verbose.printf ~flag:dbg
- "#DBG: UnifyType.f (%s) with (%s) \n"
- (Lic.string_of_type_list l1)
- (Lic.string_of_type_list l2);
- assert (List.length l1 = List.length l2);
- let res = List.fold_left2 unify_do_acc Equal l1 l2 in
- Verbose.printf ~flag:dbg
- "#DBG: UnifyType.f (%s) with (%s) gives %s\n"
- (Lic.string_of_type_list l1)
- (Lic.string_of_type_list l2)
- (string_of_t res);
- res
+ let l1_str = Lic.string_of_type_list l1 in
+ let l2_str = Lic.string_of_type_list l2 in
+
+ Verbose.printf ~flag:dbg "#DBG: UnifyType.f (%s) with (%s) \n" l1_str l2_str;
+ if (List.length l1 <> List.length l2) then
+ Ko("\n** "^ l1_str ^ " and " ^ l2_str ^ " are not unifiable (bad arity)")
+ else
+ let res = List.fold_left2 unify_do_acc Equal l1 l2 in
+ Verbose.printf ~flag:dbg
+ "#DBG: UnifyType.f (%s) with (%s) gives %s\n"
+ (Lic.string_of_type_list l1)
+ (Lic.string_of_type_list l2)
+ (string_of_t res);
+ res
(****** MATCH ASSYMETRIQUE
On le fait avec un fold_left2
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index 5dbf35d4..236aa5dc 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Fri May 31 11:27:00 2013
+Test Run By jahier on Fri May 31 15:50:19 2013
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
@@ -145,8 +145,10 @@ PASS: ./lus2lic {-o /tmp/predefOp.lic should_work/predefOp.lus}
PASS: ./lus2lic {-ec -o /tmp/predefOp.ec should_work/predefOp.lus}
PASS: ./myec2c {-o /tmp/predefOp.c /tmp/predefOp.ec}
FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/predefOp.lus
-FAIL: without any option: ./lus2lic {-o /tmp/t1.lic should_work/t1.lus}
-FAIL: Generate ec code : ./lus2lic {-ec -o /tmp/t1.ec should_work/t1.lus}
+PASS: ./lus2lic {-o /tmp/t1.lic should_work/t1.lus}
+PASS: ./lus2lic {-ec -o /tmp/t1.ec should_work/t1.lus}
+PASS: ./myec2c {-o /tmp/t1.c /tmp/t1.ec}
+PASS: ../utils/test_lus2lic_no_node should_work/t1.lus
PASS: ./lus2lic {-o /tmp/nc9.lic should_work/nc9.lus}
PASS: ./lus2lic {-ec -o /tmp/nc9.ec should_work/nc9.lus}
PASS: ./myec2c {-o /tmp/nc9.c /tmp/nc9.ec}
@@ -982,6 +984,7 @@ XFAIL: Test bad programs (syntax): lus2lic {-o /tmp/old_style_and_pack.lic shoul
XFAIL: Test bad programs (syntax): lus2lic {-o /tmp/record.lic should_fail/syntax/record.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/parametric_node3.lic should_fail/type/parametric_node3.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/parametric_node.lic should_fail/type/parametric_node.lus}
+XFAIL: Test bad programs (type): lus2lic {-o /tmp/t1.lic should_fail/type/t1.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/merge_bad_enum.lic should_fail/type/merge_bad_enum.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/condact2.lic should_fail/type/condact2.lus}
XFAIL: Test bad programs (type): lus2lic {-o /tmp/merge_bad_type.lic should_fail/type/merge_bad_type.lus}
@@ -1039,8 +1042,10 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
=== lus2lic Summary ===
-# of expected passes 879
-# of unexpected failures 87
+# of expected passes 883
+# of unexpected failures 85
# of unexpected successes 12
-# of expected failures 37
+# of expected failures 38
# of unresolved testcases 12
+testcase ./lus2lic.tests/non-reg.exp completed in 217 seconds
+testcase ./lus2lic.tests/progression.exp completed in 1 seconds
diff --git a/test/lus2lic.time b/test/lus2lic.time
index 8b80c0de..1f8391bd 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,2 +1,2 @@
-testcase ./lus2lic.tests/non-reg.exp completed in 210 seconds
-testcase ./lus2lic.tests/progression.exp completed in 0 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 217 seconds
+testcase ./lus2lic.tests/progression.exp completed in 1 seconds
diff --git a/test/should_fail/type/t1.lus b/test/should_fail/type/t1.lus
new file mode 100644
index 00000000..daa8439c
--- /dev/null
+++ b/test/should_fail/type/t1.lus
@@ -0,0 +1,44 @@
+
+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 consensus4 = consensus<<4>>;
+
+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 = 1) then a
+ else
+ fold_left << t1, t2, n-1, treat >> (
+ treat(a, X[0]),
+ X[1..n-1]
+ );
+tel
+
+node bt_void<<const n: int>>(t : bool^n) returns (x : bool);
+let
+ x = fold_left<<Lustre::or>>(false, t);
+tel
+
+(* il manque un argument boolean a ce noeud... *)
+node bt_void_bis<<const n: int>>(t : bool^n) returns (o: bool) =
+ fold_left<<bool,bool,n,Lustre::or>>;
+
+node t1 = bt_void_bis<<8>>
+
+(* node bt_void(t : bool array) = fold<<operator or>>(false, t); *)
diff --git a/test/should_work/t1.lus b/test/should_work/t1.lus
index 78359300..71f55496 100644
--- a/test/should_work/t1.lus
+++ b/test/should_work/t1.lus
@@ -19,12 +19,8 @@ node fold_left <<
type t2;
const n : int;
node treat (x:t1; y:t2) returns (z:t1)
->>
-(
- a : t1; X : t2^n
-) returns (
- c : t1
-);
+ >>
+(a : t1; X : t2^n) returns (c : t1);
let
c = with (n = 1) then a
else
@@ -40,7 +36,7 @@ let
tel
(* devrait marcher ? *)
-node bt_void_bis<<const n: int>>(t : bool^n) returns (o: bool) =
+node bt_void_bis<<const n: int>>(i : bool; t : bool^n) returns (o: bool) =
fold_left<<bool,bool,n,Lustre::or>>;
node t1 = bt_void_bis<<8>>
diff --git a/todo.org b/todo.org
index 3480ba20..0efacca0 100644
--- a/todo.org
+++ b/todo.org
@@ -3,37 +3,20 @@
* lus2lic -exec
-** oops: lus2lic internal error
- File "objlinux/data.ml", line 114, column 15
- when compiling lustre program should_work/left.lus
+** TODO Extern node not yet supported
- ./lus2lic should_work/left.lus -exec
-
-** TODO oops: lus2lic internal error
- - State "TODO" from "" [2013-05-10 Fri 18:05]
- File "objlinux/lic2soc.ml", line 680, column 18
- when compiling lustre program should_work/left.lus
-
-** TODO oops: lus2lic internal error
+oops: lus2lic internal error
- State "TODO" from "" [2013-05-13 Mon 08:11]
+
+../utils/test_lus2lic_no_node should_work/decl.lus
File "objlinux/lic2soc.ml", line 870, column 14
when compiling lustre program should_work/decl.lus
-../utils/test_lus2lic_no_node should_work/decl.lus
-** TODO oops: lus2lic internal error
- - State "TODO" from "" [2013-05-14 Tue 14:35]
+../utils/test_lus2lic_no_node should_work/simple.lus
File "objlinux/socExec.ml", line 202, column 22
when compiling lustre program should_work/simple.lus
-../utils/test_lus2lic_no_node should_work/simple.lus
-
-** TODO internal error
- - State "TODO" from "" [2013-05-10 Fri 17:19]
- File "objlinux/unifyType.ml", line 106, column 3
- ../utils/test_lus2lic_no_node should_work/t1.lus
-
-
** pb gen-autotest
../utils/test_lus2lic_no_node should_work/plus.lus
+ ./lus2lic _plus_oracle.lus -n plus_oracle -lv4 -eei -en --no-prefix -o lv4_plus_oracle.lus
diff --git a/todo.org_archive b/todo.org_archive
index 5b3236ba..8219662e 100644
--- a/todo.org_archive
+++ b/todo.org_archive
@@ -763,6 +763,61 @@ Bon, finalement, j'oblige les gens a ecrire Lustre::gt et puis ca marre.
:END:
./lus2lic _ck5_oracle.lus -n ck5_oracle -en
+* oops: lus2lic internal error
+ :PROPERTIES:
+ :ARCHIVE_TIME: 2013-05-31 Fri 13:55
+ :ARCHIVE_FILE: ~/lus2lic/todo.org
+ :ARCHIVE_OLPATH: lus2lic -exec
+ :ARCHIVE_CATEGORY: lv6
+ :END:
+ File "objlinux/data.ml", line 114, column 15
+ when compiling lustre program should_work/left.lus
+
+ ./lus2lic should_work/left.lus -exec
+
+* oops: lus2lic internal error
+ :PROPERTIES:
+ :ARCHIVE_TIME: 2013-05-31 Fri 13:56
+ :ARCHIVE_FILE: ~/lus2lic/todo.org
+ :ARCHIVE_OLPATH: lus2lic -exec
+ :ARCHIVE_CATEGORY: lv6
+ :END:
+ File "objlinux/data.ml", line 114, column 15
+ when compiling lustre program should_work/left.lus
+
+ ./lus2lic should_work/left.lus -exec
+
+* TODO oops: lus2lic internal error
+ - State "TODO" from "" [2013-05-10 Fri 18:05]
+ :PROPERTIES:
+ :ARCHIVE_TIME: 2013-05-31 Fri 13:56
+ :ARCHIVE_FILE: ~/lus2lic/todo.org
+ :ARCHIVE_OLPATH: lus2lic -exec
+ :ARCHIVE_CATEGORY: lv6
+ :ARCHIVE_TODO: TODO
+ :END:
+ File "objlinux/lic2soc.ml", line 680, column 18
+ when compiling lustre program should_work/left.lus
+
+
+* TODO internal error
+ - State "TODO" from "" [2013-05-10 Fri 17:19]
+ :PROPERTIES:
+ :ARCHIVE_TIME: 2013-05-31 Fri 15:52
+ :ARCHIVE_FILE: ~/lus2lic/todo.org
+ :ARCHIVE_OLPATH: lus2lic -exec
+ :ARCHIVE_CATEGORY: lv6
+ :ARCHIVE_TODO: TODO
+ :END:
+ File "objlinux/unifyType.ml", line 106, column 3
+ ../utils/test_lus2lic_no_node should_work/t1.lus
+
+file:src/unifyType.ml::110
+
+
+
+
+
--
GitLab